CS5030 - Automated Program Verification
Course Timings
Slot F (Tue 5 PM, Wed 11 AM, Thu 9 AM, Fri 8 AM). Online.
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 today’s world, where the boundary between safety-critical and non safety-critical applications has become vanishingly thin and the volume and complexity of software has become staggeringly large, Automated Verification has started to gain more importance. 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%35% - Class Participation: 5%
- Project: 30%
- Endsem Exam: 30%
Course Schedule (tentative)
- Assignments
- Theory Assignments: Feb 15, March 7, April 4.
- Tool Assignments: Feb 25, March 15.
- Course Project
- Proposal Due on Feb 28.
- Project Presentation in last week of semester.
- Project Report Due on May 7.
Course Textbook
- [BM] The Calculus of Computation: Decision Procedures with Applications to Verification. Aaron R. Bradley and Zohar Manna.