Atc-tutorial-proofs
ATC tutorial: ACL2 Proofs Generated for the Generated C code.
(This page may be skipped at first reading.)
Besides generating C code,
ATC also generates ACL2 proofs of
the correctness of the generated C code
with respect to the ACL2 code from which the C code is generated.
More precisely, ATC generates ACL2 theorems
that assert these correctness properties.
The correctness properties proved by ATC are the following:
- The generated C code satisfies
the compile-time constraints prescribed by [C17].
In other words, the C code is compilable by compliant compilers.
This is expressed via a formal static semantics of C.
- The generated C code is functionally equivalent
to the ACL2 code that represents it.
In other words, it computes the same things as the ACL2 code.
This is expressed via a formal dynamic semantics of C.
Previous: Approach to Generating C Code from ACL2
Next: ACL2 representation of the C int type and operations
