Automated Program Transformations

APT

Team:

We are building APT (= Automated Program Transformations), a library of tools, built on the ACL2 theorem prover, to transform programs and program specifications with a high degree of automation. The APT transformation tools operate on artifacts (e.g. functions) and generate corresponding transformed artifacts along with formal proofs of the relationship (e.g. equivalence) between old and new artifacts; all the proofs generated by APT are checked by the theorem prover. APT includes transformations to apply algorithm schemas, turn data into isomorphic representations, apply rewrite rules, incrementalize computations, turn recursion into tail recursion, and many others.

APT can be used in program synthesis, to derive provably correct implementations from formal specifications via sequences of refinement steps carried out via transformations. The specifications may be declarative or executable. The APT transformations can synthesize executable implementations from declarative specifications, as well as optimize executable specifications or implementations. The APT transformations can also be used to generate a variety of diverse implementations of the same specification. Since ACL2 includes a directly executable subset of Common Lisp, the synthesized implementations may be in ACL2, or alternatively they may be in other programming languages using code generators such as ATJ and ATC.

APT can also be used in program analysis, to help verify existing programs, suitably embedded in the ACL2 logic, by raising their level of abstraction via transformations that are inverses of the ones used in stepwise program refinement. The two kinds of transformations (for program synthesis and for program analysis) can be used together in an integrated way, as in the analysis-by-synthesis approach in the DerivationMiner project.

APT enables the user to focus on the creative parts of the program synthesis or analysis process, leaving the more mechanical parts to the automation provided by the tools. The user guides the process by choosing which transformation to apply at each point and by supplying key theorems (e.g. applicability conditions of transformations), while APT takes care of the lower-level, error-prone details with speed and assurance. We are also working on incorporating into APT heuristics to provide further automated support, e.g. to explore and automatically choose transformations. Besides automation, APT’s goals include robustness and practicality.

One of APT’s important contributions is to realize the classic ideas of program transformation and stepwise program refinement in the state-of-the-art, industrial-strength theorem prover ACL2 (which is used at AMD, Centaur, Collins Aerospace, Oracle, and others). Thus, when developing correct-by-construction programs, users can seamlessly take advantage of the theorem prover’s powerful reasoning tools, vast proof libraries, and vital user community.

We are in the process of making APT available here, as part of the ACL2 Community Books.

Also see ATJ, a Java code generator for ACL2. Also see ATC, a C code generator for ACL2. These code generators complement APT for program synthesis.

Publications

A Versatile, Sound Tool for Simplifying Definitions
Alessandro Coglio, Matt Kaufmann, Eric Smith
May 2017
14th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2017)
{Description of a tool to transform ACL2 functions definitions into simplified function definitions and to generate a proof of equivalence between old and new functions that is checked by ACL2.}

Isomorphic Data Type Transformations
Alessandro Coglio, Stephen Westfold
May 2020
16th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2020)
{Description of methods and tools to isomorphically transform data, for both program synthesis and program analysis, realized in the ACL2 theorem prover, but more generally applicable.}