CS615 : Formal Specification and Verification of Programs 2019

Instructor : Ashutosh Gupta

Timings : 15:30 Tuesday and Friday
Venue : CC105

Source material

Evaluation structure

May change later.

Lectures

The following lecture schedule is tentative

Programs

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

2019-08-09 : Lecture 2 - Strongest post

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

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

Engineering Verification tools

2019-08-20 : Lecture 5 - SMT Solvers

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

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

Theory of abstraction

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

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

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

2019-09-10 : (holiday)

2019-09-13 : Lecture 10 - Maps

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

2019-09-17/20 : midterm week

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

Abstract interpretation

2019-09-27 : Lecture 13 - Abstract interpretation

2019-10-01 : Lecture 14 - Abstract domains: box and octagon

2019-10-04 : Lecture 15 - Abstract domains: polyhdera

2019-10-08 : (holiday)

2019-10-11 : Lecture 16 - Domain combinations

Model checking

2019-10-15 : Lecture 17 - Model checking

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

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

2019-10-25 : Lecture 20 - CEGAR

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