CS 525, Formal Methods for System Verification

 Winter 2018-2019

Instructor 

Purandar Bhaduri, ext: 2360, email: pbhaduri

Teaching Assistants

  1. Ramanuj Chouksey (email: r.chouksey)

  2. Dipojjwal Ray (email: dipojjwal)

  3. Prasita Mukherjee (email: prasi174101042)

  4. Salihundam Baby Sai Sameera (email: samee174101035)

Textbook

Principles of Model Checking, Christel Baier and Joost-Pieter Katoen, MIT Press, May 2008.

Evaluation

Assignments    15%

Midsem           35%

Endsem           50%

 

Midsem Solutions

 

Endsem Solutions

Some Useful Links

Courses on Verification

  1. Course on Introduction to Model Checking at Aachen, 2016 by Joost-Pieter Katoen.

  2. Course on Advanced Model Checking at Aachen, 2017 by Joost-Pieter Katoen.

  3. Course on Verification at Universität des Saarlandes, 2011-2012 by Bernd Finkbeiner, Peter Faymonville and Michael Gerke.

  4. Course on Bug Catching: Automated Program Verification and Testing at CMU, 2014 by Ed Clarke.

  5. Course on Introduction to Model Checking at CMU, 2014 by Ed Clarke.

  6. Course on Computer-Aided Verification at UPenn, 2016 by Rajeev Alur.

Satisfiability Modulo Theories (SMT)

  1. Tutorial on SAT: Beyond Propositional Satisfiability by Roberto Sebastiani in CADE 2003.

  2. Satisfiability Modulo Theories, Clark W. Barrett and Cesare Tinelli, in Handbook of Model Checking, (Ed Clarke, Thomas Henzinger, and Helmut Veith, eds.), 2017.

  3. Tutorial slides on Satisfiability Modulo Theories by Clark Barrett, Sixth Summer School on Formal Techniques, May  2016.

  4. Tutorial slides on SMT Solvers: Theory and Practice by Clark Barrett, Summer School on Verification Technology, Systems & Applications, September 2008.

  5. Tutorial slides on Modern SMT Solvers and Verification by Sayan Mitra at the GIAN course on Modeling and Verification of Cyber-Physical Systems, IIT Guwahati, January 2018.

  6. A tutorial on Satisfiability Modulo Theories (Invited Tutorial), Leonardo de Moura, Bruno Dutertre, and Natarajan Shankar, in Computer Aided Verification, 19th International Conference, CAV 2007, volume 4590 of Lecture Notes in Computer Science, pages 20-36. Springer, 2007. Slides based on the tutorial by Natarjan Shankar.

  7. Satisfiability Modulo Theories: An Appetizer, Leonardo de Moura and Nikolaj Bjørner, SBMF 2009: Formal Methods: Foundations and Applications pp 23-36, LNCS 5902, Springer, 2009.

  8. Satisfiability modulo theories: introduction and applications, Leonardo de Moura and Nikolaj Bjørner, CACM Vol 54, Issue 9, 2011.

  9. SAT/SMT by Example by Dennis Yurichev.

  10. Tutorial slides on SAT/SMT Solvers and Their Applications by Ashutosh Gupta.

  11. Nikolaj Bjørner's page on SMT and Z3.

  12. Couse on Automated Reasoning, 2018 by Ashutosh Gupta.

Tutorial and Survey Papers

  1. Linear-Time Temporal Logic and Büchi Automata, Tutorial talk by Madhavan Mukund, Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, January 1997. 

  2. Finite-state Automata on Infinite Inputs, Madhavan Mukund, Modern Applications of Automata Theory, World Scientific (2012) 257-288.  

  3. Model-checking: Automated Verification of Computational Systems, Madhavan Mukund, Resonance, July 2009.

Homeworks

HW#1: Due date: Monday, 28 January 2019.  You have to give a demo of your solutions to a TA in the lab

This is an exercise using the SMT solver Z3. Download and install Z3 from here. You can read about how to use Z3 from Getting Started with Z3: A Guide. There is also a tutorial on programming Z3 using Python which you can read about from here. You can find many other useful stuff at the Z3 Wiki. Once you are familiar with the tool, solve these exercises using Z3. Note that to handle loops you have to unroll them to the single static assignment (SSA) representation of programs. See Example 1.1 on page 8 of Applications of SMT solvers to Program Verification.

HW#2: Due date: Monday, 11 February 2019. Problems 2.1, 2.5, 2.9 and 2.12 from here.

HW#3: Due date: Monday, 25 February 2019. Problems 3.1, 3.4, 3.5, 3.7 and 3.10 from here.

HW#4: Due date: Monday, 25 March 2019 [Mini-project].  This exercise involves using the NuSMV model checker to verify the correctness of a distributed algorithm. Download and install the NuSMV tool. Learn about how to use the tool from the tutorial and user manual. Then use SMV processes (i.e., with interleaving rather than synchronous concurrency) to model and verify a solution by Sukumar Ghosh to Dijkstra's stabilizing token ring algorithm. You can find another description of this algorithm here (Section 17.3.2).
  1. You need to state and verify the obvious safety and liveness properties (see the second reference) and also the self-stabilization property (also called convergence in the second reference) of the algorithm.
  2. You should try to verify the algorithm for four processes, and then see what happens when you increase the number of processes.
  3. You should think about the fairness assumptions that are necessary for the verification.
  4. You will be required to give a demo to the TAs and answer questions about your work.

HW#5: Due date: Tuesday, 16 April, 2019. Problems 4.1, 4.6, 4.9, 4.11 and 4.14 from here.

HW#6: Due date: Monday, 29 April, 2019. Problems 5.1, 5.2, 5.11 and 5.13 from here.

Homework Policy

Late assignments would be penalised by deducting (10 × no. of days of lateness) % of the marks. Any form of copying will incur zero marks.

 back to homepage