CS 56000: Reasoning about Programs

Course Description:

The course focuses on the logical foundations and algorithmic techniques used to ensure program correctness. With an emphasis on automated program verification and synthesis, the course covers classical concepts and techniques such as Hoare logic, abstract interpretation, abstraction-refinement and bounded model checking. The course also exposes students to approaches for program synthesis – a new frontier for program reasoning -  such as inductive synthesis, synthesis using version space algebras, constraint-based synthesis and synthesis based on machine-learning techniques. The courses emphasizes both theoretical foundations as well as hands-on experience with verification/synthesis tools and SAT/SMT solvers.   

Course Outline:

Unit 1: Introduction, Logics, Proof Engines, Core Techniques (Weeks 1- 4)

What is program verification? What is program synthesis? Why should we care about automated reasoning about programs? Overview of reasoning techniques, success stories.

Review of propositional logic. A treatment of first-order logic and first-order theories.

A brief look at satisfiability solvers and satisfiability modulo theory solvers. Decision procedure for a core theory.

Introduction to program verification and correct specifications via Hoare logic. Preconditions, postconditions, Hoare triples, weakest preconditions, strongest postconditions, invariants, verification conditions, method of inductive assertions.

Unit 2: Sequential Programs: Verification and Analysis (Weeks 4-6)

In-depth look at automated invariant generation via abstract interpretation, fixed-point computation for overapproximation of reachable states

Abstraction-refinement for improving precision of abstraction, predicate abstraction

Bounded model checking.

Unit 3: Concurrent Programs: Verification and Analysis (Weeks 6-7)

Overview of the challenges of dealing with concurrency. Common concurrency bugs and synchronization primitives. Overview of different verification and analysis techniques for concurrent programs.

In-depth treatment of the Owicki-Gries proof-based technique for verification of concurrent programs.

In-depth treatment of symbolic predictive analysis for concurrent programs.

Unit 4: Program Synthesis (Weeks 8-14)

Introduction to program synthesis and overview of techniques.

Inductive synthesis, programming by example, Enumerative search. Search based on version-space algebras. Constraint–based search. Counterexample-guided inductive synthesis (CEGIS).

Functional synthesis using CEGIS. Functional synthesis using method of inductive assertions.

Machine learning based synthesis approaches.

Synthesis for concurrency.

Introduction to automated program repair. Program repair based on program distances.