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.
Originalsprog | Engelsk |
---|---|
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 |
Antal sider | 4 |
Vol/bind | 320 |
Forlag | EPTCS |
Publikationsdato | 7 aug. 2020 |
Sider | 155-158 |
DOI | |
Status | Udgivet - 7 aug. 2020 |
Begivenhed | 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis - Dublin, Irland Varighed: 25 apr. 2020 → 26 apr. 2020 Konferencens nummer: 8+7 |
Workshop
Workshop | 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis |
---|---|
Nummer | 8+7 |
Land/Område | Irland |
By | Dublin |
Periode | 25/04/2020 → 26/04/2020 |
Navn | Electronic Proceedings in Theoretical Computer Science |
---|---|
Vol/bind | 320 |
ISSN | 2075-2180 |