Polyvariant program specialisation with property-based abstraction

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

Resumé

In this paper we show that property-based abstraction, an established technique originating in software model checking, is a flexible method of controlling polyvariance in program specialisation in a standard online specialisation algorithm. Specialisation is a program transformation that transforms a program with respect to given constraints that restrict its behaviour. Polyvariant specialisation refers to the generation of two or more specialised versions of the same program code. The same program point can be reached more than once during a computation, with different constraints applying in each case, and polyvariant specialisation allows different specialisations to be realised. A propertybased abstraction uses a finite set of properties to define a finite set of abstract versions of predicates, ensuring that only a finite number of specialised versions is generated. The particular choice of properties is critical for polyvariance; too few versions can result in insufficient specialisation, while too many can result in an increase of code size with no corresponding efficiency gains. Using examples, we show the flexibility of specialisation with property-based abstraction and discuss its application in control flow refinement, verification, termination analysis and dimension-based specialisation.
OriginalsprogEngelsk
TitelEPTCS 299 : Proceedings Seventh International Workshop on Verification and Program Transformation
Antal sider15
ForlagEPTCS
Publikationsdato2019
DOI
StatusUdgivet - 2019
BegivenhedSeventh International Workshop on Verification and Program Transformation - Co-Located with the 3rd International Conference on the Art, Science, and Engineering of Programming (Programming 2019), Genova, Italien
Varighed: 2 apr. 20192 apr. 2019
http://refal.botik.ru/vpt/vpt2019/

Workshop

WorkshopSeventh International Workshop on Verification and Program Transformation
LokationCo-Located with the 3rd International Conference on the Art, Science, and Engineering of Programming (Programming 2019)
LandItalien
ByGenova
Periode02/04/201902/04/2019
Internetadresse

Citer dette

Gallagher, J. P. (2019). Polyvariant program specialisation with property-based abstraction. I EPTCS 299: Proceedings Seventh International Workshop on Verification and Program Transformation EPTCS. https://doi.org/10.4204/EPTCS.299.6
Gallagher, John Patrick. / Polyvariant program specialisation with property-based abstraction. EPTCS 299: Proceedings Seventh International Workshop on Verification and Program Transformation. EPTCS, 2019.
@inproceedings{e841c34c70c64fdba060547fc8fcfc1e,
title = "Polyvariant program specialisation with property-based abstraction",
abstract = "In this paper we show that property-based abstraction, an established technique originating in software model checking, is a flexible method of controlling polyvariance in program specialisation in a standard online specialisation algorithm. Specialisation is a program transformation that transforms a program with respect to given constraints that restrict its behaviour. Polyvariant specialisation refers to the generation of two or more specialised versions of the same program code. The same program point can be reached more than once during a computation, with different constraints applying in each case, and polyvariant specialisation allows different specialisations to be realised. A propertybased abstraction uses a finite set of properties to define a finite set of abstract versions of predicates, ensuring that only a finite number of specialised versions is generated. The particular choice of properties is critical for polyvariance; too few versions can result in insufficient specialisation, while too many can result in an increase of code size with no corresponding efficiency gains. Using examples, we show the flexibility of specialisation with property-based abstraction and discuss its application in control flow refinement, verification, termination analysis and dimension-based specialisation.",
keywords = "program transformation, Partial evaluation, Program verification",
author = "Gallagher, {John Patrick}",
year = "2019",
doi = "10.4204/EPTCS.299.6",
language = "English",
booktitle = "EPTCS 299",
publisher = "EPTCS",

}

Gallagher, JP 2019, Polyvariant program specialisation with property-based abstraction. i EPTCS 299: Proceedings Seventh International Workshop on Verification and Program Transformation. EPTCS, Genova, Italien, 02/04/2019. https://doi.org/10.4204/EPTCS.299.6

Polyvariant program specialisation with property-based abstraction. / Gallagher, John Patrick.

EPTCS 299: Proceedings Seventh International Workshop on Verification and Program Transformation. EPTCS, 2019.

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

TY - GEN

T1 - Polyvariant program specialisation with property-based abstraction

AU - Gallagher, John Patrick

PY - 2019

Y1 - 2019

N2 - In this paper we show that property-based abstraction, an established technique originating in software model checking, is a flexible method of controlling polyvariance in program specialisation in a standard online specialisation algorithm. Specialisation is a program transformation that transforms a program with respect to given constraints that restrict its behaviour. Polyvariant specialisation refers to the generation of two or more specialised versions of the same program code. The same program point can be reached more than once during a computation, with different constraints applying in each case, and polyvariant specialisation allows different specialisations to be realised. A propertybased abstraction uses a finite set of properties to define a finite set of abstract versions of predicates, ensuring that only a finite number of specialised versions is generated. The particular choice of properties is critical for polyvariance; too few versions can result in insufficient specialisation, while too many can result in an increase of code size with no corresponding efficiency gains. Using examples, we show the flexibility of specialisation with property-based abstraction and discuss its application in control flow refinement, verification, termination analysis and dimension-based specialisation.

AB - In this paper we show that property-based abstraction, an established technique originating in software model checking, is a flexible method of controlling polyvariance in program specialisation in a standard online specialisation algorithm. Specialisation is a program transformation that transforms a program with respect to given constraints that restrict its behaviour. Polyvariant specialisation refers to the generation of two or more specialised versions of the same program code. The same program point can be reached more than once during a computation, with different constraints applying in each case, and polyvariant specialisation allows different specialisations to be realised. A propertybased abstraction uses a finite set of properties to define a finite set of abstract versions of predicates, ensuring that only a finite number of specialised versions is generated. The particular choice of properties is critical for polyvariance; too few versions can result in insufficient specialisation, while too many can result in an increase of code size with no corresponding efficiency gains. Using examples, we show the flexibility of specialisation with property-based abstraction and discuss its application in control flow refinement, verification, termination analysis and dimension-based specialisation.

KW - program transformation

KW - Partial evaluation

KW - Program verification

U2 - 10.4204/EPTCS.299.6

DO - 10.4204/EPTCS.299.6

M3 - Article in proceedings

BT - EPTCS 299

PB - EPTCS

ER -

Gallagher JP. Polyvariant program specialisation with property-based abstraction. I EPTCS 299: Proceedings Seventh International Workshop on Verification and Program Transformation. EPTCS. 2019 https://doi.org/10.4204/EPTCS.299.6