An experiment combining specialization with abstract interpretation

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearch

Documents

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.
Original languageEnglish
Title of host publicationProceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis
Number of pages4
PublisherarXiv.org
Publication date2020
Pages155-158
DOIs
Publication statusPublished - 2020
Event8th International Workshop on Verification and Program Transformation, VPT 2020 and 7th Workshop on Horn Clauses for Verification and Synthesis, HCVS 2020 - Dublin, Ireland
Duration: 25 Apr 202026 Apr 2020

Conference

Conference8th International Workshop on Verification and Program Transformation, VPT 2020 and 7th Workshop on Horn Clauses for Verification and Synthesis, HCVS 2020
LandIreland
ByDublin
Periode25/04/202026/04/2020
SeriesElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume320
ISSN2075-2180

ID: 305531910