CS5030 - Automated Program Verification

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. In addition, the course will also involve reading the latest research papers in the area.

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 (tentative)

  • Assignments: 30%
  • Project: 40%
  • Final Exam: 30%

Course Schedule

  • Assignments
    • Assignment 1: Out on Sep 28, Due Oct 7 Due Oct 11
    • Assignment 2: Out on Oct 26, Due Nov 4
  • Course Project
    • Proposal Due on Oct 18
    • Project Presentation in First Week of December
    • Project Report Due on Dec 6
  • Final Exam
    • Take-home exam in the week of Dec 7