Fall 2018 Course Descriptions

COMP 150-02 Program Analysis, Verification, and Synthesis

J. Foster
MW 3:00-4:15, Halligan Hall 111A
I+ Block

The idea of software—the interchangeable instructions that control general-purpose computing devices—is one of the major breakthroughs of Computer Science. While we often think of software as human-generated text, in fact from the earliest days of computing, when compiler technology was first developed, researchers have been exploring ways to manipulate and reason about software algorithmically.

In this class, we will study three closely related topics that arose out of this research. We will begin with program analysis, which initially was developed to enable compilers to perform optimization. Today, program analyses are also used to solve a range of software engineering problems, including finding bugs and security vulnerabilities. Next, we will study program verification, which aims to prove that programs are correct. In recent years, researchers have built verified compilers, operating systems, cryptography libraries, and others. Finally, we will study program synthesis, which searches for a program satisfying a specification. Researchers have demonstrated synthesis of synchronization for high-performance parallel code, program inverses, fast Fourier transforms, and more. Program synthesis even underlies the Flash Fill feature of Microsoft Excel.

Each of these topics could be a course on its own, so the goal of this class is to give students a broad overview of these areas and the relationships between them. Throughout the course, students will design an implement basic program analysis, verification, and synthesis tools, and study the theory behind them.

Prerequisite: COMP 105, graduate standing, or instructor consent.

Back to Main Courses Page