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.
|Titel||Proceedings of VPT/HCVS@ETAPS 2020 : 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis|
|Redaktører||Laurent Fribourg , Matthias Heizmann|
|Status||Udgivet - 2020|
Gallagher, J. P., & Glück, R. (2020). An Experiment Combining Specialization with Abstract Interpretation. I L. Fribourg , & M. Heizmann (red.), Proceedings of VPT/HCVS@ETAPS 2020: 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis (Bind 320, s. 155-158). EPTCS. https://arxiv.org/abs/2008.02937v1