22904 Computer-Aided Verification of Hardware and Software

Credits: 4 graduate credits in Computer Science

Prerequisite: Admission to the graduate program in Computer Science 1

The course is based on Logic in Computer Science: Modelling and Reasoning about Systems, by M. Huth and M. Ryan (Cambridge University Press, 2004), and on “Symbolic model checking without BDDs,” by A. Biere, A. Cimatti, E. Clarke & Y. Zhu, in Proc. Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS (Amsterdam, 1999).

Many critical systems use software and hardware components that are characterized by extremely complex behavior and have to meet very high reliability requirements. The course examines how to ensure that such a system meets given specifications, using model checking. This is essentially different from testing a system because testing does not provide proof of a system's correctness.

Topics: Temporal logics: CTL and LTL; Automata-based model checking; Various model checking algorithms and their complexity; Addressing the state explosion problem: symbolic model checking using binary decision diagrams, bounded model checking; Automatic tools for model checking.

---

1Students who have not fulfilled this requirement may, under certain circumstances, enroll in this course.