ACL2 To C
- 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.
A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2
17th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2022)