ACL2 To C

Team:

• Alessandro Coglio (Lead)
• Ruben Gamboa
• Grant Jurgensen
• James McDonald
• Karthik Nukala
• Eric Smith

We are building ATC (= ACL2 To C), a proof-generating C code generator for the ACL2 theorem prover. ATC translates ACL2 code of a specified form into C, and it also generates an ACL2 proof of correctness of the generated C code with respect to the ACL2 code, based on a formal model of C that we are also developing in ACL2.

ATC complements APT. These two tools provide a way to synthesize verified C code from high-level specifications.

ATC is available here and documented here.

Also see ATJ, a Java code generator for ACL2.

Publications

A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2
Alessandro Coglio
May 2022
17th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2022)