Description: 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 emphasize 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.
CourseContent:
- Foundations, Semantics and Specification of Programs, Hoare Logic, Weakest Pre-condition, Strongest Post-Condition, Inductive Invariants, Examples (2 Weeks)
- SAT and SMT solvers, Constraint-based Verification, Program Verification using Constrained Horn Clauses (CHC) (2 Weeks)
- Abstract Interpretation, Lattices, Galois Connection, Knaster Tarski Fixpoint Theorem, Widening and Narrowing Operators, Abstract Domains : Interval, Hexagon, Octagon, Polyhedra (4 Weeks)
- Bounded Model Checking, Symbolic Model Checking, Counter Example Guided Abstraction Refinement (CEGAR) (2 Weeks)
- Predicate Abstraction, Boolean Programs, Craig Interpolation (2 Weeks)
- Automated Invariant Generation: Property Directed Reachability, Machine Learning-based techniques (2 Weeks)
TextBooks:Aaron R. Bradley and Zohar Manna, The Calculus of Computation: Decision Procedures with Applications to Verification,Springer, Berlin, Heidelberg. ISBN 978-3-540-74112-1 (2007).
Reference Books:Ranjit Jhala and Rupak Majumdar. Software Model Checking. ACM Computing Surveys (CSUR) 41.4 (2009): 1-54. Edmund M. Clarke, Thomas Henzinger, Helmut Veith, Roderick Bloem. "Handbook of Model Checking. Springer, Cham. ISBN:978-3-319-10574-1 (2018).
