E0 223 Verification

• Course outline
  • Temporal Logic based verification:
    • Introductory automata concepts
    • Buchi automata
    • Linear Temporal Logic (LTL)
    • Modelling systems
    • Computation Tree Logic (CTL)
    • Symbolic model checking
    • Tools: Spin, SMV
  • Verification of infinite-state systems
    • Verification of real-time systems
      • Timed automata
      • Modelling real-time systems
      • Tools: Uppaal, Kronos
    • Verification of pushdown systems, Software verification
    • Verification of security protocols

  • Texts and other material
    • Clarke, Grumberg, Peled: Model Checking
      
    • Berard, Bidoit, Finkel, et al: Systems and Software Verification
    • Wolfgang Thomas: Automata on Infinite Objects, in Handbook of Theoretical Computer Science, Elsevier 1990.
    • Some partial lecture notes (last updated on 14 Feb 2006).
    • Madhavan Mukund: Finite-state Automata on Infinite Inputs
    • Madhavan Mukund: Linear-Time Temporal Logic and Buchi Automata
    • John Rushby: Mechanised Formal Methods: Progress and Prospects
    • Courcoubetis et. al: Memory Efficient Algorithms for the Verification of Temporal Properties
    • Spin stuff:
      • Spin website: spinroot.com.
      • Spin 4.0.1 tar-ball.
      • Chapter 4 of Holzmann's book on validation of protocols.
      • Some sample spin programs: non-det.s, mutual-exclusion.s, crossing.s, ltl property for crossing.s.
    • Allen Emerson's article on Temporal Logic in Handbook of TCS:
    • Randy Bryant: Graph-Based Algorithms for Boolean Function Manipulation.
    • SMV: tared binaries (also contains html version of tutorial and language reference. Hard copies available with me.)
    • Hubert Comon's slides on "Automatic Verification of Cryptographic Protocols", CIMPA school, Bangalore.
    • Rusinowitch and Turuani: Protocol Sessions with finite number of sessions is NP complete.
    • Alur and Dill: A theory of timed automata.
    • Uppaal binaries.
    • direct proof of non-closure under complementation for timed automata (from Sunil Simon's MSc report).

  • Material for Sriram Rajamani's lectures on Program Analysis & Verification
    • Plan of Lectures

      Date	Speaker	Topic
      Mon Jan 23	Sriram Rajamani	Abstract interpretation (introduction)
      Mon Jan 30	Sriram Rajamani	Abstract interpretation (general formulation, widening and narrowing)
      Thu Feb 2	Sriram Rajamani	Discussion on abstract interpretation and homework
      Thu Feb 9	Aditya Nori	Interprocedural analysis - Sharir Pnueli
      Mon Feb 20	Aditya Nori	Interprocedureal analysis - Sharir-Pnueli
      Thu Mar 2	Aditya Nori	Interprocedureal analysis - Sharir-Pnueli
      Thu Mar 9	Sriram Rajamani	Flow insensitive analyses
      Thu Mar 16	Sriram Rajamani	Context Sensitive Analysis.
      Thu Mar 30	Sriram Rajamani	Predicate abstraction

    • Slides for lectures
      • Lecture 1 (Sriram): PPT version, PDF version
      • Lecture 2 (Sriram): PPT version, PDF version
      • Lecture 3 (Aditya): PPT version, PDF version.
      • Lecture 4 (Aditya): PDF version Lecture 5 (Sriram): PDF version.
      • Lecture 6 (Sriram): PDF version.

    • Other material
      • Abstract Interpretation: A unified lattice model... Patrick Cousot and Radhia Cousot, ACM POPL'77.
      • Points-to analysis in almost linear time, Bjarne Steensgaard, POPL '96.
      • Lecture 6 is based on the paper: Cloning-based Context Sensitive Pointer Analysis using Binary Decision Diagrams by Whaley and Lam, PLDI 2004.

  • Assignments

  • Seminar topics
    1. Memory Efficient cycle detection (Anand Bhalgat and Sriraghavendra, Fri 27th Jan, 3:30pm).
    2. Safra's Construction for complementing Buchi automata (Rathijit Sen, Fri 10th Feb, 3:30pm). Safra's paper.
    3. Buchi's Monadic Second Order Logic (Raveendra and Sudipta, Fri 3rd Mar).
    4. Expressive Completenes of LTL (V. Deepak and Vamsi Krishna) and .
    5. Bounded Model Checking (Rogers Matthew and Mathew Francis) Paper (see also BCCSZ-Advances-2003)
    6. Linear and Branching Temporal Logic (Amareshwari and Megha).
    7. Automated analysis of Hybrid Systems (Tarun and Laxmi).

  • Proposed weightage for evaluation:
    • Mid-semester Exam: 20%
    • Assignments (Lab + written): 40%
    • Final Exam: 40%

  • Meeting schedule: Tue & Thu, 11:30am, and Mon 5:30pm (Sriram Rajamani's lectures), all in CSA Seminar Room. First meeting on Tue, 10th Jan 2006.

  • Exam Schedule:
    • Mid-semester Exam: 3:30pm, Fri 10 March 2006.
    • Final Exam: 10:00am, Thu 27th April 2006.