CS 6115

Certified Software Systems

Cornell University · UGRD · Fall 2026

1 section

Catalog description

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.

Sections

Current meeting, instructor, credit, and enrollment details

Updated 8 hours ago

001

Availability not recently verified

Class #cornell_2-CS6115Fall 2026UGRD4 credits

Days & times: No scheduled meeting time
Meeting dates: —
Location: —
Instructor: Staff

Class numbers and section codes come from the registrar.

Spot missing or incorrect course data?