E0 323: Topics in Verification


August - December 2011
Instructors: Aditya Kanade, Satish Chandra (IBM Research)
Office Hours: Wednesdays: 5pm - 6pm
(by prior email appointment)
Timings:
Wednesdays: 10am - 11.30am
Fridays: 10am - 11.30am
Classroom: 225



Announcements




Introduction


A holy grail of computer science is to automate programming and associated software engineering tasks performed by humans. For example, static program analysis can automatically discover certain properties of programs. Software testing has long been an object of automation.

In this course, we aim to study algorithmic approaches for automating

These are useful and, at the same time, challenging tasks to automate. The proposed techniques in literature draw from many sub-areas in computer science, including programming languages, formal methods, and machine learning. We aim to cover applications of such techniques to diverse domains such as bit-vector and array-manipulating programs, spreadsheets, concurrent and parallel programs, and software libraries.

Along with presentations by course instructors, every participant will be assigned a few papers to be presented in the class. The exchange of knowledge will be mainly through open discussions in the classes. An optional course project will be offered for interested participants. 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 instructors.

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. The presentation of a paper will take 2 classes (3 hours) approximately.

Synthesis of programs
P1. Combinatorial sketching of finite programs (Satish)
P2. Deriving linearizable fine-grained concurrent objects (Arnab)
P3. Learning programs from traces using version space algebra (Aditya)
P4. Spreadsheet table transformations from examples (Sumesh)
P5. A genetic programming approach to automated software repair (Omesh)
P6. From program verification to program synthesis (Shalini)

Mining specifications of programs
P7. Mining specification (Sumesh)
P8. Synthesis of interface specifications for Java classes (Aravind)
P9. Static specification mining using automata-based abstractions (Jay)
P10. Jungloid mining: helping to navigate the API jungle (Omesh)

Selection of domain-specific data structures and algorithms
P11. Context-sensitive domain-independent algorithm composition and selection (Sumesh)
P12. A framework for adaptive algorithm selection in STAPL (Rajesh)
P13. Data representation synthesis (Omesh)