Sequential Program Verification and Analysis

Wednesday, 5:00-7:00 PM
Room 1003, 715 Broadway
Amir Pnueli

Reaching Me

Amir Pnueli

Prerequisites: Some background in algorithm design, familiarity with the language of first-order logic, and at least one imperative and one functional programming language.

Course requirements: Assignments and a term project.


Course Description

The course will introduce the basic approaches to program verification, which is the process by which one can formally specify the expected behavior of a program and formally verify that the program meets its specification.

Class Presentations


  • Assignment 2 -- April 2, 2003, revised Apr. 18, 2003: