CS615 : Formal Specification and Verification of Programs 2019

Instructor : Ashutosh Gupta

Timings : 15:30 Tuesday and Friday
Venue : CC105

Source material

Survey: Software model checking
Book: Model Checking Clarke, Grumberg and Peled
Text: Lattice theory for computer science Hilary A. Priestley
Abstract interpretation
The octagon abstract domain. Antoine Mine. In HOSC 2006
The Art of Multiprocessor Programming by Nir Shavit
Book: Theory of Linear and Integer Programming, Alexander Schrijver
Various papers

Evaluation structure

Programming assignments: 5% 15% 15% 10%
Quizzes : 10% (5% each)
Midterm : 20% (2 hour)
Presentation: 10% (15 min) (distritubted over the semester!)
Final: 15% (2 hour)

May change later.

Lectures

The following lecture schedule is tentative

Programs

2019-07-30 : Lecture 1 - Introduction to verification

Intrdoction to verification, and course content
A simple language and small-step semantics
slides

2019-08-09 : Lecture 2 - Strongest post

Strongest post, least fixed points
slides

2019-08-13 : Lecture 3 - Weakest pre and Hoare logic

slides

2019-08-16 : Lecture 4 - Labeled transition systems and invariants

slides

Engineering Verification tools

2019-08-20 : Lecture 5 - SMT Solvers

Using Z3 SMT solver
slides

2019-08-23 : Lecture 6 - Advanced encoding of problems

Quiz 1
slides

2019-08-27 : Lecture 7 - LLVM Intermediate representation

A compiler support for Verification
slides
llvm-demo.tar (For untar: tar -xvf llvm-demo.tar)

Theory of abstraction

2019-08-30 : Lecture 8 - Why abstraction?

Reachability for invariants
Abstraction
slides

2019-09-03 : (cancelled due to student request)

2019-09-06 (make up lecture): Lecture 9 - Lattice

partial orders, Poset, Semi-lattice, and lattice
Assignment 1 due!
slides

2019-09-10 : (holiday)

2019-09-13 : Lecture 10 - Maps

Monotonicity, order embeddings, continous maps, closure operators
slides

2019-09-15 (make up lecture): Lecture 11 - Fixed points

Knaster-Tarski theorem, iterates
Conditions for reaching fixedpoints
slides

2019-09-17/20 : midterm week

2019-09-24 : Lecture 12 - Galois connection and abstraction

slides

Abstract interpretation

2019-10-08 : (holiday)

2019-10-11 : Lecture 16 - Domain combinations

slides

Model checking

2019-10-15 : Lecture 17 - Model checking

slides

2019-10-18 : Lecture 18 - Hardware model checking - BDD

Quiz 2
slides

2019-10-22 : Lecture 19 - Bounded model checking

slides

2019-10-25 : Lecture 20 - CEGAR

slides

2019-10-28 (Monday): (cancelled due to Diwali)

2019-11-01 : Lecture 21/22 - Refinement

2019-11-05 : Lecture 23 - Student presentations

2019-11-08 : Lecture 24 - Industry talk or Beyond safety: Termination

Presentation topics

Please look into the program of the following two conferences and choose a paper to present. Please let me know your choice. It would be best if you actively consult the instructor for the decision.

Student presentation schedule

The students are allowed to borrow slides from the internet, authors of the reference, or any other source, with clear citation. However, it is their responsibility that ideas are clearly presented during the presentation. The presentation should be about 25-30mins long.

	Date	Student	Topic
1	2019-11-05	Vrunda	SAT-Based Model Checking Without Unrolling, Understanding IC3 by Aaron R. Bradley
2	2019-11-05	Shreyash M	Decidable Verification of Uninterpreted Programs,UMANG MATHUR*, University of Illinois, Urbana Champaign,P. MADHUSUDAN,MAHESH VISWANATHAN
3	2019-11-05	Shreyash P	Program synthesis
4	2019-11-05	Kalyani
5	2019-11-05	Chanchal	Bayes meets Dijkstra: Verifying Bayes Networks by Program Verification
6	2019-11-05	Sapta	Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement,Nick Giannarakis,Ryan Beckett,Ratul Mahajan,David Walker
7	2019-11-05