Prerequisite: CMSC330; or students who have taken courses with comparable content may contact the department; or permission of instructor.
Topics in program verification. Operational semantics of programs. Preconditions and postconditions. Axiomatic proof systems and predicate transformers. Temporal logic and model checking. Process algebra, semantic equivalences and algebraic reasoning.