Introduction to formal specification, analysis, and verification of computer system behavior. Topics include formal logical reasoning about computer programs and systems, automated and semi-automated verification, and algorithmic methodologies for ascertaining that a computing system satisfies its formally specified properties.