An Experiment Combining Specialization with Abstract Interpretation

John Patrick Gallagher, Robert Glück

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

Abstract

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.
OriginalsprogEngelsk
TitelProceedings of VPT/HCVS@ETAPS 2020 : 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis
RedaktørerLaurent Fribourg , Matthias Heizmann
Vol/bind320
ForlagEPTCS
Publikationsdato2020
Sider155-158
DOI
StatusUdgivet - 2020
Begivenhed8th International Workshop on
Verification and Program Transformation
and 7th Workshop on
Horn Clauses for Verification and Synthesis
- Dublin, Irland
Varighed: 25 apr. 202026 apr. 2020
Konferencens nummer: 8+7

Workshop

Workshop8th International Workshop on
Verification and Program Transformation
and 7th Workshop on
Horn Clauses for Verification and Synthesis
Nummer8+7
LandIrland
ByDublin
Periode25/04/202026/04/2020
NavnElectronic Proceedings in Theoretical Computer Science
Vol/bind320
ISSN2075-2180

Citer dette