CS 6115 (Spring 2015)

Certified Software Systems
TR 8:40-9:55
Hollister 406


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 participation and a substantial course project.


Nate Foster
Email: jnfoster[at]cs.cornell.edu
Office Hours: Monday 4pm-5pm

Validate XHTML Validate CSS
Last updated January 2015