CS 6115

Last Updated

  • Schedule of Classes - June 22, 2015 4:42PM EDT
  • Course Catalog - June 11, 2015 6:21PM EDT

CS 6115
Certified Software Systems

Course information provided by the 2014-2015 Catalog.

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.


Prerequisites/Corequisites Prerequisites: CS 6110 or permission of the instructor.

When Offered Fall.

View Enrollment Information

Syllabi: none

  •   Regular Academic Session. 

  • 4 Credits Graded

  • 16827 CS 6115   SEM 101

  •  

  • Instruction Mode: In Person