E0 223 Verification

Topics covered

• Introductory automata concepts
• Buchi automata
• Linear Temporal Logic (LTL)
• Computation Tree Logic (CTL)
• Symbolic model checking
• Tools: Spin, SMV
• Timed automata
• Timed temporal logics

Texts and references

• Class notes

Assignments

• Assignment 1
• Assignment 2
• Assignment 3
• Assignment 4
• Assignment 5
• Assignment 6

Exams

• Mid-Semester Exam
• Final Exam

Links

• Spin

Seminars

• Memory efficient cycle detection (Anand Bhalgat and Sriraghavendra)
• Safra's construction for complementing Buchi automata (Rathijit Sen)
• Buchi's Monadic Second Order Logic (Raveendra and Sudipta)
• Expressive Completeness of LTL (Deepak.V and Vamsi Krishna)
• Bounded Model Checking (Rogers Matthew and Mathew Francis)
• Linear and Branching Temporal Logic (Amareshwari and Megha)
• Automated analysis of Hybrid Systems (Tarun and Laxmi)

Lectures on Program Analysis & Verifcation
(Sriram Rajamani/Aditya Nori)

• Topics covered
• Abstract interpretation
• Interprocedural analysis
• Flow-insensitive analysis
• Context-sensitive analysis
• Slides
• Lecture 1
• Lectures 2 & 3
• Lectures 4 & 5
• Lecture 6
• Lecture 7
• References
• Patrick Cousot, Radhia Cousot, Abstract interpretation : A unified lattice model for static analysis of programs by construction or approximation of fixpoints
• M Sharir, A Pnueli, Two approaches to interprocedural data flow analysis
• Bjarne Steensgaard, Points-to Analysis in Almost Linear Time
• John Whaley, Monica S. Lam, Cloning-Based Context-Sensitive Pointer Alias Analysis Using Binary Decision Diagrams
• Assignment