CS652: Computer Aided Verification

Monsoon 2019 (July 29, 2019 - November 14, 2019)

Lecture Hours: Monday and Thursday 10:35 am to 11:50 am
Office Hour: Thursday 5:00 pm to 6:00 pm

Lecture Venue: KD 102

Instructor: Indranil Saha (Email: isaha[at]cse[dot]iitk[dot]ac[dot]in)

Teaching Assistants:
Tanmoy Kundu (Email: tanmoy[at]cse[dot]iitk[dot]ac[dot]in)
Ratijit Mitra (Email: ratijit[at]iitk[dot]ac[dot]in)


Overview

Correctness of the hardware, software and cyber-physical systems is of prime importance to prevent financial loss or loss of life. With the increase in the complexity of the systems, ensuring the correctness of the systems becomes a significant 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 specification. The course will also look into various software tools that have been successful in utilizing the algorithmic techniques to solve practical verification problem.


Prerequisites

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 familiarity with finite state machines and ordinary differential equations, and programming experience will be helpful.


Topics

  • Modeling of Systems: Modeling of concurrent systems, timed systems, hybrid systems and probabilistic systems.
  • Specification Languages: Linear time properties, regular properties, Linear Temporal Logic (LTL), Computation 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, Satisfiability Solvers, Satisfiability Modulo Theories (SMT) Solvers.
  • Software Tools: Popular formal methods tools such as Spin, NuSMV, SAL, UPPAAL, SpaceX, Prism, Z3 and CUDD.


    • Grading Policy

    Assignments - 40%
    Mid-Semester Examination - 20%
    End-Semester Examination - 30%
    Class Attendance - 10%

    Our department follows this anti-cheating policy strictly.


    Assignment and Exam Schedule

    Homework Assignments
    Spin Assignment (Released: August 12, 2029; Deadline: September 13, 2019)
    NuSMV Assignment (Released: September 29, 2029; Deadline: October 20, 2019)
    SAT and SMT Assignment (Released: October 19, 2029; Deadline: November 08, 2019)
    UPPAAL Assignment (Released: October 26, 2029; Deadline: November 15, 2019)
    Research Paper presentation

    Mid-Semester Examination
    September 20, 2019 (Friday) 6:00 pm to 8:00 pm in KD102

    Final Examination
    November 19, 2019 (Tuesday) 4:00 pm to 7:00 pm at KD102


    Lecture Schedule

    Lecture Date Main Topic Sub Topic References
    1July 29, 2019 Modelling Concurrent Systems Introduction to Systems Verification, The Model Checking Process, Transition Systems, Modeling Hardware Systems [BK08: Ch1, Ch2]
    2August 1, 2019 Modeling Data Dependent Systems, Concurrency and Interleaving, Communication with Shared Variables [BK08: Ch2]
    3August 5, 2019 Handshaking, Synchronous Parallelism, Channel Systems [BK08: Ch2]
    4August 8, 2019 Introduction to Promela and Spin, The State-Space Explosion Problem [BK08: Ch2]
    5August 19, 2019 Linear Time Properties Deadlock, Linear-Time Behavior, Safety Properties and Invariants [BK08: Ch3]
    6August 22, 2019 Liveness Properties, Fairness [BK08: Ch3]
    7August 26, 2019 Regular Properties Automata on Finite Words, Regular Safety Properties, Verifying Regular Safety Properties, [BK08: Ch4]
    8August 29, 2019 omega-Regular Languages and Properties, NBA, DBA [BK08: Ch4]
    9September 2, 2019 GNBA, Model-Checking omega-Regular Properties [BK08: Ch4]
    10September 5, 2019 Linear Temporal Logic Syntax and Semantics, Equivalence of LTL Formulae [BK08: Ch5]
    11September 9, 2019 Fairness in LTL, Automata-Based LTL Model Checking [BK08: Ch5]
    12September 12, 2019 Automata-Based LTL Model Checking (Contd.) [BK08: Ch5]
    Mid-Semester Examination
    13September 23, 2019 Computation Temporal Logic Syntax and Semantics of CTL, Expressiveness of CTL vs. LTL [BK08: Ch6]
    14September 26, 2019 CTL Model Checking, Fairness in CTL [BK08: Ch6]
    15September 30, 2019Binary Decision Diagram, Symbolic CTL Model Checking [BK08: Ch6], [Bry86]
    16October 3, 2019 SAT and SMT SAT and SMT Solvers [NOT06], [BSST09], [dMB08]
    Mid-Semester Recess
    17October 14, 2019 Equivalence and Abstraction Bisimulation [BK08: Ch7]
    18October 17, 2019 Simulation Relations [BK08: Ch7]
    19October 21, 2019 Stutter Linear-Time Relations [BK08: Ch7]
    22October 24, 2019 Timed Automata Syntax and Semantics Timed Automata [BK08: Ch9]
    23October 25, 2019 Timed Computation Tree Logic, TCTL Model Checking [BK08: Ch9], [AD94]
    20October 28, 2019 Partial Order Reduction Independence of Actions, Ample Set Constraints, Dynamic Partial Order Reduction [BK08: Ch8]
    21November 1, 2019 Computing Ample Sets, Static Partial Order Reduction [BK08: Ch8]
    24November 11, 2019
    Paper Presentations by Students
    25November 12, 2019
    26November 14, 2019
    Final Examination


    References

    [BK08] C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.
    [CGP99] E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.
    [NOT06] R. Nieuwenhuis, A. Oliveras, C. Tinelli. Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T). J. ACM 53(6): 937-977, 2006.
    [BSST09] C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability modulo theories. In Armin Biere, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 4, chapter 8. IOS Press, 2009.
    [dMB08] L. M. de Moura and N. Bjorner. Z3: An efficient smt solver. In TACAS, pages 337-340, 2008.
    [AD94] Rajeev Alur, David L. Dill: A Theory of Timed Automata. Theor. Comput. Sci. 126(2): 183-235, 1994.
    [Bry86] R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, 35(8):677-691, 1986.
    [Ras05] Jean-Francois Raskin. An Introduction to Hybrid Automata. Handbook of Networked and Embedded Control Systems, pages 491-517, 2005.
    [BCC+03] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu: Bounded model checking. Advances in Computers 58: 117-148 (2003)