C2C

Team:

• Alessandro Coglio
• Grant Jurgensen
• Eric Smith

We are building C2C (= C To C), a toolkit to transform C code according to a variety of criteria. For a subset of the C language, C2C also generates proofs of correctness each time a transformation runs.

C2C is implemented using the ACL2 theorem prover. The proofs that it generates are in the language of ACL2 and are checked by ACL2. The basis for the proofs is our semantics for a subset of C, which C2C shares with ATC.

C2C is available here and documented here.

Also see ATC, a proof-generating C code generator for ACL2.