- Schedule of Classes - June 22, 2015 4:42PM EDT
- Course Catalog - June 11, 2015 6:21PM EDT
Course information provided by the Courses of Study 2014-2015.
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.
When Offered Fall.
Prerequisites/Corequisites Prerequisites: CS 6110 or permission of the instructor.
Credits and Grading Basis
4 Credits Graded(Graded)
Class Number & Section Details
- TRHollister Hall 306
Or send this URL: