(CS60030) FORMAL SYSTEMS
Spring 2015
Instructors
Dipankar Sarkar, Soumyajit Dey
Office: Room {115, 306}, CSE Building
Email: {ds, soumya} @ cse.iitkgp.ernet.in
Class Timing
MON(09:30-10:30), WED(07:30- 08:30), WED(08:30-09:30), THURS(09:30-10:30)
Venue:: CSE-108
Teaching Assistants
Soumyadip Bandyopadhyay, Antonio Bruto da Costa
Email: {antonio.cse.iitkgp, soumyadip.bandyopadhyay } @ gmail.com
Approximate Coverage (DS)
1. Property Verification
-------------------------
Transition Systems, Temporal Logics :: CTL, LTL, CTL* and Model Checking; -- 10 lectures
Timed Automata -- Modelling, TCTL, TLTL, Model Checking -- 5 lectures
2. Functional Verification
--------------------------
Progam Verification -- Flowchart Verification -- Partial Correctness, Termination, Floyd-Hoare Axiomatic Systems -- 4 lectures
3. Behavioural Verification
---------------------------
Bisimulation equivalence checking of Transition Systems -- 5 lectures
Approximate Coverage (SD)
4. Abstract Interpretation of Programs
--------------------------------------
Mathematical foundations, Order-theoretic approximations (abstraction, closures, Galois connections, fixpoint abstraction, widening, narrowing, refinement),
Design of a generic structural abstract interpreter (collecting semantics, non-relational and relational analysis, convergence acceleration by widening/narrowing),
Static analysis (forward reachability analysis, backward analysis, iterated forward/backward analysis, termination),
Numerical abstract domains (intervals, affine equalities, congruences, octagons, polyhedra);
-- 8 lectures
5. Hybrid System verification
-----------------------------
Hybrid Automata, Decidability / undecidability issues, Approximate Reachability Analysis, Zeno Behaviour -- 7 lectures
Evaluation :
Mid-sem (30 Marks), End-Sem (50) marks , TA (20 marks)
TA marks dsistribution: 5 (weekly assignments) + 15 for 2 class tests
-------------------------------------------------------------------------------
Total lecture hours : 39 lectures
Tutorial Classes -- every week -- class + home assignment : 13 classes
-------------------------------------------------------------------------------
Total : 52 classes
Reference Material:
For Property Verification and Behavioural Verification:
-------------------------------------------------------
1. Christel Baier and Joost-Pieter Katoen -- Principles of Model Checking, The MIT Press Cambridge, Massachusetts, London, England, 2008.
2. Michael Huth and Mark Ryan -- Logic in Computer Science : Modelling and Resoning about Systems, Cambridge Univ. Press, 2004.
3.E, M. Clark, Jr., O. Grumberg, D. A. Peled -- Model Checking, The MIT Press Cambridge, Massachusetts, London, England, 1999.
For Functional Verification:
---------------------------
4. Zohar Manna -- Mathematical Theory of Computation, McGraw-Hill Kogakusha, Tokyo, 1974.
Abstract Interpretation:
-----------------------
5. Jan Midtgaard's Course on Abstract Interpretation
6. Patrick Cousot's Abstract Interpretation course at MIT
7. Relevant Material - maintained by the founder himself
8. Relevant Material - by Neilson
Hybrid Systems:
---------------
9. The Theory of Hybrid Automata (1996) - Thomas A. Henzinger
10. The algorithmic analysis of hybrid systems (1995) - R. Alur et. al.
11. Logical Analysis of Hybrid Systems