C0: Specification and Verification in
Introductory Computer Science

C0 is a small safe subset of the C programming language, augmented with contracts, specifically developed for teaching the course 15-122 Principles of Imperative Computation at Carnegie Mellon University.

C0 has not yet been publicly released, but beta distributions (binary only) are now available on the Downloads page.

Many people have contributed to C0 and its tool suite. The principal designers are Rob Arnold and Frank Pfenning; additional contributors include Laura Abbott, Tom Cortina, Jason Koenig, William Lovas, Karl Naden, Rob Simmons, Nathan Snyder, Anand Subramanian, and Jakob Uecker.

The development of C0 and the 15-122 course curriculum has been supported by the MSR-CMU Center for Computational Thinking under a project on Specification and Verification in Introductory Computer Science and by a gift from Google for the development of CMU's introductory undergraduate courses.

Frank Pfenning