ACL2 To C
Team:
- Alessandro Coglio (Lead)
- 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.