CS 6115 - Certified Software Systems

Overview

In recent years, it has become practical to build large software systems using formal proof assistants. Examples of such certified systems include the seL4 microkernel, the CompCert C compiler, the Vellvm LLVM compiler, and the Bedrock library. This course provides a hands-on introduction to programming using the Coq proof assistant. Assessment is based on class participation, presentations, homeworks, and a course project.

Logistics

9:40am-10:55am Tuesday & Thursday in Upson 146.

Instructor

Nate Foster
jnfoster@cs.cornell.edu

Office Hours

1:30-2:30pm Wednesdays in Gates 432. Also by appointment.

Discussion

Please use Ed to discuss course-related content.