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
    • 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 11 Feb 2005).
    • 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 website: spinroot.com. Spin 4.0.1 tar-ball.
    • Spin tutorial (by B. Meenakshi): Talk 1 and Talk 2.
    • 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 numer 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).

  • Assignments
    • Assignment 1.
      Solutions by Madhu Gopinathan.
    • Assignment 2.
      Solutions by Madhu Gopinathan.
    • Assignment 3 (due on Wed 9 March).
      Solutions by Madhu Gopinathan.
    • Assignment 4 (due on Tue 15 March).
      More on alternating bit protocol from Chapter 4 of Design and Validation of Computer Protocols by G. Holzmann.
    • Assignment 5 (due on Mon 18 April).
    • Assignment 6 (Not required to be submitted).

  • Seminar topics
    1. Memory Efficient cycle detection, Prateem Mandal, Mon 7 Feb 2005, 5pm.
    2. Safra's Construction for complementing Buchi automata, Debamalya Panigrahi, 14 Feb, 5pm.
    3. Expressive Completenes of LTL, Pavithra Prabhakar, Mon 28th Feb, 5pm.
    4. Buchi's Monadic Second Order Logic, Subhashree and Sowjanya.
    5. CTL Satisfiability problem, Joy Chakraborty.
    6. Proof Carrying Code S. Roopesh and Vishal Sharda.
    7. Bounded Model Checking, Prakash and Manikantan.
    8. Automated analysis of Hybrid Systems, Arnab De and Anand.

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

  • Meeting schedule: Tue & Thu, 11:30am, in CSA Seminar Room. First meeting on Tue, 11th Jan 2005.

  • Exam Schedule:
    • Mid-semester Exam: 11:30am Thursday 10 Mar 2005.
    • Final Exam: 2:00pm Monday 25th April 2005.