Automated reasoning and program verification 2016

Instructor : Ashutosh Gupta

Timings : Monday 11:00 - 12:30 and 14:00 - 15:30
Venue : A-203

This course is divided in two modules, namely automated reasoning and program verification. Automated reasoning will include advance design of SAT solvers, theory combination, decision procedures for various first-order theories, proof generation, maxsat, model counting, quantifier elimination, interpolation, abduction, etc. Program verification will include program modelling, concolic testing, abstract interpretation, symbolic model checking, bounded model checking, abstract refinement based model checking, concurrency verification, and termination proving. The course work will include theoretical as well as practical exercises.

Source material

• Survey: Software model checking
• Book: Decision Procedures
• Book: Logic in Computer Science Huth and Ryan
• Book: Model Checking Clarke, Grumberg and Peled

Evaluation structure

• Assignments : 40% (4% each - 10 assignments)
• Midterm : 20% (1 hour)
• Presentation : 10% (15 min)
• Final project : 30%

Lectures

Module : Program verification

2016-02-01 : Week 1 - Program and property modelling

• Course content and logistics
• Program modeling - A simple language
• Operational semantics
• Big and small step semantics
• Logical representation of program statements
• Strongest post and weakest pre condition
• Slides(last slide contains the assignment)

2016-02-08 : Week 2 - Explicit and symbolic methods

• Hoare logic
• Labelled transition system
• Invariant checking, annotation
• Explicit model checking
• Symbolic model checking
• Constraint based invariant generation
• Slides(last topic contains the assignment)

Module : Automated reasoning

2016-02-15 : Week 3 - SMT solvers reminder, EUF, Z3

• SMT solving
• Theory solver interface
• Theory of equality and function symbols(EUF)
• Union-find for EUF
• Z3 implementation of EUF
• Slides(last topic contains the assignment)

2016-02-22 : Week 4 - Decision procedures - linear rational arithmetic(LRA)

• Fourier-Motzkin
• Incremental simplex
• Geometric intuition of simplex
• Termination of simplex
• notes on incremental simplex
• Slides(assignment is exercises 2.4-6)

2016-02-29 : Week 5 - Decision procedures - octagonal constraints

• Cooper's method for linear integers arithmetic (Manna slides)
• Integer/Rational difference logic(IDL/RDL)
• Octagonal constraints
• The octgon abstract domain(read it after week 8)
• Slides(assignment is exercises 3.10,12,13)

2016-03-07 : Week 6 - Threory of arrays and theory combination

• Theory of arrays
• Theory combination
• The Nelson-Oppen Method for theory combination
• Slides(assignment: exercises 4.5,4.7,4.8)
• Z3 Arrays(section 2-4)
• Clark Barrett slides for Nelson-Oppen

2016-03-14 : Midterm

Module : Program verification (contd.)

2016-03-21 : Week 7 - Lattice theory and fixed points

• Poset
• Lattice
• Maps
• Galois connection
• Fixed points
• Slides(assignment: exercises 3.3,3.9,3.10)

2016-03-28 : Week 8 - Abstract interpretation

• Abstract interpretation
• Abstract domains
• Widening/Narrowing operators
• Box domain
• Octagonal domain
• Polyhedra domain
• Slides(assignment: exercises 4.8,4.13,4.14)

2016-04-04 : Week 9 - Abstract model checking and termination

• Abstract program
• Predicate abstraction
• Abstract reachability graph
• Counter example guided abstraction refinement
• Slides(assignment: exercises 5.6-5.8)

2016-04-11 : Week 10 - Linear temopral logic and Buchi automaton

• Delivered by Paritosh

Module : Automated Reasoning (contd.)

2016-04-18: Week 11 - Proof generation and interpolation

• Resolution proofs in SMT solvers
• Proof formats
• Minimizing proofs
• Proofs in LRA
• Interpolation
• Interpolation for propositional logic
• Interpolation for LRA
• Proofs slides
• Interpolation slides(assignment: exercise 5.5)

2016-04-25: Week 12 - Verification using Coq

• Student presentations - Theory of bit-vectors - Rahul
• Student presentations - Owicki-Gries proof system for concurrent programs - Gunjan
• Mechanized semantics - Xavier Leroy

2016-05-13 : Project submission deadline

Student presentation