Proving Skipping Refinement with ACL2s

Mitesh Jain
(Northeastern University)
Panagiotis Manolios
(Northeastern University)

We describe three case studies illustrating the use of ACL2s to prove the correctness of optimized reactive systems using skipping refinement. Reasoning about reactive systems using refinement involves defining an abstract, high-level specification system and a concrete, low-level system. Next, one shows that the behaviors of the implementation system are allowed by the specification system. Skipping refinement allows us to reason about implementation systems that can "skip" specification states due to optimizations that allow the implementation system to take several specification steps at once. Skipping refinement also allows implementation systems to, i.e., to take several steps before completing a specification step. We show how ACL2s can be used to prove skipping refinement theorems by modeling and proving the correctness of three systems: a JVM-inspired stack machine, a simple memory controller, and a scalar to vector compiler transformation.

In Matt Kaufmann and David L. Rager: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2015), Austin, Texas, USA, 1-2 October 2015, Electronic Proceedings in Theoretical Computer Science 192, pp. 111–127.
Published: 18th September 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.192.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org