CS5030 - Automated Program Verification
Course Timings
Slot F (Tue 5 PM, Wed 11 AM, Thu 9 AM, Fri 8 AM). CS24
Course Overview
Automated Verification of programs has often been called the holy grail of computer science. While undecidable in general, over the years, a number of elegant techniques have been developed to solve this problem for several useful classes of programs. In this course, we will go through a wide spectrum of techniques used in the domain of Automated Verification. The course will emphasise on both theory and practice, with hands-on experience of some of the tools used in this domain.
Course Contents
-
Preliminaries:SAT and SMT - Propositional Logic: Syntax and Semantics, Resolution-based SAT solving, DPLL, First-Order Logic: Syntax and Semantics, Satisfiability Modulo Theories, First Order Theories
-
Program Semantics and Specifications - Operational Semantics, Strongest Post-condition and Weakest Pre-condition, Hoare Logic
-
Automated Techniques - Abstract Interpretation, Bounded Model Checking, Predicate Abstraction, CEGAR, Property-Directed Reachability
Grading Policy
- Assignments [3 Theory + 2 Tool]: 40%
- Class Participation: 5%
- Paper Reading: 25%
- Endsem Exam: 30%
Course Schedule (tentative)
- Assignments (release weeks are mentioned below)
- Theory Assignments: Feb 6, March 6, April 10.
- Tool Assignments: Feb 20, March 20.
- Paper Reading
- Paper selection to be finalized by middle of March.
- Paper presentation in the last week of the semester.
Course Textbook
- [BM] The Calculus of Computation: Decision Procedures with Applications to Verification. Aaron R. Bradley and Zohar Manna.
Course Moodle Page
https://coursesnew.iitm.ac.in/course/view.php?id=1267 (self-enroll is enabled).