Title: Computer Aided Veri_cation
Course No: CS636 (Suggested)
Units: 3-0-0-0-9
Pre-requisites: The course does not have any formal prerequisites. The students are expected to have
mathematical maturity of the level of an undergraduate degree in engineering. However, some fa-
miliarity with _nite state machines and theory of computation, and programming experience will be
helpful.
Proposed by: Indranil Saha
Estimated Enrollment: 30
Other faculty members who could be interested in teaching the course: Prof. Amey Karkare (CSE),
Prof. Subhajit Roy (CSE), Prof. Anil Seth (CSE), Prof. Sandeep K. Shukla (CSE), Prof. Sunil Simon
(CSE) and others
Departments which may be interested: Electrical Engineering, Mechanical Engineering, Aerospace En-
gineering, Mathematics
Level of the course: PG (6xx level).
Correctness of the hardware, software and cyber-physical systems is of prime importance to prevent _nancial
loss or loss of life. With the increase in the complexity of the systems, ensuring the correctness of the systems
becomes a signi_cant challenge and entails algorithmic methods that can automatically ensure correctness
of the systems without manual intervention. This course will discuss the mechanisms for modeling a system
and capturing its requirements formally, and algorithms and techniques for verifying the model with respect
to its formal speci_cation. The course will also look into various software tools that have been successful in
utilizing the algorithmic techniques to solve practical veri_cation problem.
Modeling of Systems: Modeling of concurrent systems, timed systems, hybrid systems and probabilistic
systems.
Speci_cation Languages: Linear time properties, regular properties, Linear Temporal Logic (LTL), Com-
putation Tree Logic (CTL), Timed Computation Tree Logic (TCTL), Probabilistic Computational Tree
Logic (PCTL)
Techniques for Model Checking: Explicit-State Model Checking, Symbolic Model Checking, Bounded
Model Checking, Equivalence and Abstraction, Partial Order Reduction
BDD, SAT and SMT: Binary Decision Diagrams, Satis_ability Solvers, Satis_ability Modulo Theories
(SMT) Solvers.
Software Tools: Popular formal methods tools such as Spin, NuSMV, SAL, UPPAAL, SpaceX, Prism, Z3
and CUDD.
[BK08] C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.
[CGP99] Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, 1999.
[RP] Relevant research papers.