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 software system satisfies its formally specified properties. Cannot be taken for credit in addition to the course with the same number formerly entitled "Object-Oriented Software Principles."