An Experiment Combining Specialization with Abstract Interpretation

John P. Gallagher
(Roskilde University, Denmark and IMDEA Software Institute, Spain)
Robert Glück
(Copenhagen University, Denmark)

It was previously shown that control-flow refinement can be achieved by a program specializer incorporating property-based abstraction, to improve termination and complexity analysis tools. We now show that this purpose-built specializer can be reconstructed in a more modular way, and that the previous results can be achieved using an off-the-shelf partial evaluation tool, applied to an abstract interpreter. The key feature of the abstract interpreter is the abstract domain, which is the product of the property-based abstract domain with the concrete domain. This language-independent framework provides a practical approach to implementing a variety of powerful specializers, and contributes to a stream of research on using interpreters and specialization to achieve program transformations.

In Laurent Fribourg and Matthias Heizmann: Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis (VPT/HCVS 2020), Dublin, Ireland, 25-26th April 2020, Electronic Proceedings in Theoretical Computer Science 320, pp. 155–158.
Published: 7th August 2020.

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