Fall Semester, 2004
One of the major research thrusts in programming language technology today is for improving our ability to discover and verify properties of programs. The set of available techniques range from the inexpensive but limited type checking to the expensive and comprehensive theorem proving. The ideal balance between cost and expressiveness is being approached from these two extremes. In this course we will position ourselves on the theorem proving side but we will hold cost-effectiveness as an important goal.
We will start with the exploration of a set of traditional techniques from theorem proving and logic, such as natural deduction, and resolution theorem provers. Then we move beyond propositional and first-order logic and explore automatic decision procedures that are customarily used to reason about programs: equality, linear arithmetic, pointer based data-structures. We will explore these decision procedures in the context of cooperative decision-procedure theorem provers, such as the Nelson-Oppen prover (used by the ESC/Java system) and the Shostak theorem prover (used in the PVS system). Then, we will talk about interactive theorem provers (such as PVS and Coq).
Additional topics to be covered in the third part of the course: boolean abstraction (as in BLAST and SLAM), randomized decision procedures, procedures for verifying pointer-based programs, SAT-based deduction, and others.
We will implement a theorem prover consisting of a Nelson-Oppen core for cooperating decision procedures along with a series of individual decision procedures.
Tuesdays and Thursdays, 12:30 - 2:00, 310 Soda
|
Instructor |
Admin. Assistant |
Liliana Gonzales |
|
|
|
Office: 783 Soda |
|
Office: 776 Soda |
|
|
Phone: 643-1481 |
|
Phone: 642-8395 |
|
|
Email: necula @ cs |
|
Email: lilianag@cs |
|
|
Office hours: T 2-3, and by appointment |
|
|
Most materials will be posted on the main course web page (http://www.cs.berkeley.edu/~necula/autded).
There are no required texts. A number of research papers will be handed out in class as the course progresses.
Course work will include reading, a small number of homework assignments, and a term project. Students taking the class for credit will have to deliver one lecture based on a couple of research papers. There will be no exams.
The project is intended to give you hands on experience with the material taught in the course and with the practical issues involved in the implementation of decision-procedure based mechanical theorem provers. I will provide a common core that allows a large class of independent decision procedures to cooperate towards proving a goal. Then we will split into groups and each group will program a decision procedure of their choice.
The project will be implemented in the Objective CAML dialect of ML. OCAML is a statically typed functional language with powerful modularity support, object-oriented support and a strong development environment including interfacing with C, a profiler and even a back-stepping debugger. Its automatic memory management, a rich language of types and the pattern matching support make it an ideal implementation language for any symbolic computation task, such as theorem provers, program analyzers or compilers.
The assignments and the project will be weighted roughly equally in determining the final grade.
There are no formal prerequisites for this course. However, students with some background in formal reasoning (in the style taught in CS263 for example) will find it easier to grasp the material in the beginning. Since the project will be implemented in Objective CAML (OCAML) dialect of ML, it is helpful to have previous programming experience in Standard ML or OCAML. For those of you who are not familiar with ML programming I will distribute tutorials and will even hold a couple of tutorial lectures, if necessary.