E0 323: Topics in Verification


August - December 2010
Instructor: Aditya Kanade
Timings:
Tuesdays: 2pm-3.30pm
Thursdays: 2pm-3.30pm
Classroom: 252



Introduction


Formal verification is an exciting and fast-moving field of research. It borrows and contributes ideas to many other areas of computer science e.g. automata theory, machine learning. In this course, we will study some classical and some recent papers in formal verification applied to software. The themes of this year are: program synthesis, applications of learning theory to verification, and interprocedural analysis. Every participant will be assigned some papers to be presented in the class and will also be required to make a presentation on his/her ongoing research work.

The pre-requisites for taking this course are Program Analysis and Verification (E0 227) or Automated Verification (E0 223). In other cases, you can seek permission from the instructor.

Course contents


The list of papers that we want to study in this course is given below. Name of the person presenting the paper is mentioned in parentheses. Everyone else participating in the course is also expected to read the paper before the presentation and engage in active participation in the class.

Program synthesis

P1: Representation dependence testing using program inversion (Aditya)
P2: From program verification to program synthesis (Anirudh)
P3: Complete functional synthesis (Pranavadatta)
P4: Abstraction-guided synthesis of synchronization (Arnab)

Applications of learning theory to verification

P5: Statistical debugging: simultaneous identification of multiple bugs (Praveen)
P6: The Daikon system for dynamic detection of likely invariants (Praveen)
P7: Learning regular sets from queries and counter-examples (Pranavadatta)
P8: Grey-box checking (Anirudh)

Interprocedural analysis

Pre-requisite reading: Two approaches to interprocedural data-flow analysis (covered in E0 227)
P9: Precise interprocedural dataflow analysis via graph reachability (Rajesh)
P10: Weighted pushdown systems and their application to interprocedural dataflow analysis (Mallesham)
P11: Bebop: a path-sensitive interprocedural dataflow engine (Anirudh)
P12: Analysis of recursive state machines (Vasanta)

Presentations on current work

One lecture by each participant (approximately 8-10 lectures in all)