CS652: Computer Aided Verification

Fall 2017 (July 31, 2017 - November 15, 2017)

Lecture Hours: Wednesday and Friday 5 pm to 6:30 pm
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)
Guest Instructor: Ansuman Banerjee (Email: ansuman[at]isical[dot]ac[dot]in)

Teaching Assistants: Surajit Ghosh (Email: surajg[at]cse[dot]iitk[dot]ac[dot]in)
Souradeep Chandra (Email: soura[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 - 20%
    Project - 30%
    Mid-Semester Examination - 20%
    End-Semester Examination - 30%

    Our department follows this anti-cheating policy strictly.


    Assignment and Exam Schedule

    Homework Assignments
    Spin Assignment
    SAT and SMT Assignment
    UPPAAL Assignment

    Project
    Project Proposal Submission (Deadline: September 17, 2017)
    Intermediate Project Presentation (Scheduled on October 18 2017 and October 20, 2017)
    Final Project Presentation (Scheduled on November 10, 2017, November 15, 2017)
    Final Report Submission (Deadline: November 17, 2017)

    Mid-Semester Examination
    September 17, 2017 (Sunday) 8:00 am to 10:00 am at KD102

    Final Examination
    November 18, 2017 (Saturday) 4:00 pm to 7:00 pm at KD102


    Lecture Schedule

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


    Projects

    List of Projects
    Exploration of Verification Issues Related to Cloud Computing Using Homemade Hardware Shutter (Siddharth Srivastava and Nishant Anand)
    Verification Of Consensus In Blockchain (Ras Dwivedi and Vikas Sheel Parashar)
    Verification of Probabilistic Realtime Systems: A Survey (Pranjal Choubey and Upendra Prasad)
    Formal Verification of Artificial Neural Networks: A Survey (Pratyush Varshney and Saket Arya)
    Modeling and Verification of Hybrid Systems using SpaceX: A Survey (Ratijit Mitra and Vivek Kumar Yadav)
    Unified Payment Interface: Modeling and Verification of the Technical Specification (Shubham Sahai Srivastava)
    Energy-Aware Temporal Logic Motion Planning for Mobile Robot (Tanmoy Kundu)


    Project Grading Scheme
    Your project will be graded out of 30 based on the following scheme:
    Proposal - 5
    Intermediate Project Presentation - 10
    Final Project Presentation - 15



    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. Bjørner. 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.