E0 223 Verification
Temporal Logic based verification:
Introductory automata concepts
Linear Temporal Logic (LTL)
Computation Tree Logic (CTL)
Symbolic model checking
Tools: Spin, SMV
Verification of real-time systems
Modelling real-time systems
Tools: Uppaal, Kronos
- Texts and other material
- Assgnment 1.
- Assgnment 2.
- Assgnment 3.
- Assgnment 4.
- Assgnment 5.
- Seminar topics
- Safra's Construction for complementing Buchi automata
(Mangesh Gupte, 5 Feb 2004).
See also: Determinisation of Buchi Automata by Markus
- Memory Efficient cycle detection (Pannagadatta, Fri 20
- Buchi's Monadic Second Order Logic (Murali Krishnan,
Fri 19 March 2004)
- Minimizing Buchi automata (Shailesh Patil, Thu 01 Apr 2004)
- Automata-theoretic approach to CTL (Madhu Gopinathan,
Fri 02 Apr 2004)
- Temporal Logic can be more expressive (Raj Mohan, Fri 9 Apr)
- Bounded Model Checking, (Gaurav Malhotra, Fri 16 Apr)
- Zone algorithm for timed automata (Deepak Bharadwaj,
Thu 22 Apr)
- Automated analysis of Hybrid Systems (M. P. Dushyant, Fri 23 Apr)
Proposed weightage for evaluation:
Mid-semester Exam: 20%
Assignments (Lab + written): 40%
Final Exam: 40%
Meeting schedule: Tue & Thu, 11:30am, in CSA Seminar
- Exam Schedule:
Mid-semester Exam: 11:30 am, Thursday 4th March, 2004.
Final Exam: 10:00 am Thu 29 April 2004.