Automated Program Transformations
- Kestrel Institute
- University of Texas at Austin
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.
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, Oracle, Rockwell Collins, 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.
A Versatile, Sound Tool for Simplifying Definitions
Alessandro Coglio, Matt Kaufmann, and Eric Smith
14th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2017)