CS 525, Formal Methods for System Verification

 Spring 2017-2018

Instructor 

Purandar Bhaduri, ext: 2360, email: pbhaduri

Teaching Assistants

  1. Ramanuj Chouksey (email: r.chouksey)

  2. Dipojjwal Ray (email: dipojjwal@iitg.ernet.in)

Textbooks

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

  2. M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Second Edition, Cambridge University Press, 2005. (Available in South Asian edition)

Evaluation

Assignments    15%

Midsem            35%

Endsem            50%

 

Midsem Solutions

Endsem Solutions

Some Useful Links

  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.

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

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

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

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

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

Homeworks

  1. HW#1: Problems 2.1, 2.3, 2.5, 2.9 and 2.12 from here. Due date: 12 February, 2018.

  2. HW#2: Problems 3.4, 3.5, 3.6, 3.11 and 3.13 from here. Due date: 26 February, 2018.

  3. HW#3: [Mini Project, Due: 16 April, 2018] 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 Dijkstra's stabilizing token ring algorithm. You may find this version more readable than Dijkstra's original paper.
    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. For extra credit, model and verify the synchronous version of the algorithm, where all processes execute their steps in a lock-step fashion.
    5. You will be required to give a demo to the TAs and answer questions about your work.
  4. HW#4: Problems 4.1, 4.6, 4.9, 4.11 and 4.14 from here. Due date: 11 April, 2018.

     

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