CS652: Computer Aided Verification

 

1 Administrative Information

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).

 

2 Course Details

2.1 Short Description

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.

 

2.2 Topics

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.

 

References

[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.