TU Darmstadt / ULB / TUbiblio

Certified Abstract Cost Analysis

Albert, Elvira ; Hähnle, Reiner ; Merayo, Alicia ; Steinhöfel, Dominic
Guerra, Esther ; Stoelinga, Marielle (eds.) (2021):
Certified Abstract Cost Analysis.
In: Lecture Notes in Computer Science, 12649, In: Fundamental Approaches to Software Engineering, pp. 24-45,
Springer, 24th International Conference of the European Joint Conferences on Theory and Practice of Software, virtual Conference, 27.03.-01.04.2021, DOI: 10.1007/978-3-030-71500-7\_2,
[Conference or Workshop Item]

Abstract

A program containing placeholders for unspecified statements or expressions is called an abstract (or schematic) program. Placeholder symbols occur naturally in program transformation rules, as used in refactoring, compilation, optimization, or parallelization. We present a generalization of automated cost analysis that can handle abstract programs and, hence, can analyze the impact on the cost of program transformations. This kind of relational property requires provably precise cost bounds which are not always produced by cost analysis. Therefore, we certify by deductive verification that the inferred abstract cost bounds are correct and sufficiently precise. It is the first approach solving this problem. Both, abstract cost analysis and certification, are based on quantitative abstract execution (QAE) which in turn is a variation of abstract execution, a recently developed symbolic execution technique for abstract programs. To realize QAE the new concept of a cost invariant is introduced. QAE is implemented and runs fully automatically on a benchmark set consisting of representative optimization rules.

Item Type: Conference or Workshop Item
Erschienen: 2021
Editors: Guerra, Esther ; Stoelinga, Marielle
Creators: Albert, Elvira ; Hähnle, Reiner ; Merayo, Alicia ; Steinhöfel, Dominic
Title: Certified Abstract Cost Analysis
Language: English
Abstract:

A program containing placeholders for unspecified statements or expressions is called an abstract (or schematic) program. Placeholder symbols occur naturally in program transformation rules, as used in refactoring, compilation, optimization, or parallelization. We present a generalization of automated cost analysis that can handle abstract programs and, hence, can analyze the impact on the cost of program transformations. This kind of relational property requires provably precise cost bounds which are not always produced by cost analysis. Therefore, we certify by deductive verification that the inferred abstract cost bounds are correct and sufficiently precise. It is the first approach solving this problem. Both, abstract cost analysis and certification, are based on quantitative abstract execution (QAE) which in turn is a variation of abstract execution, a recently developed symbolic execution technique for abstract programs. To realize QAE the new concept of a cost invariant is introduced. QAE is implemented and runs fully automatically on a benchmark set consisting of representative optimization rules.

Book Title: Fundamental Approaches to Software Engineering
Series: Lecture Notes in Computer Science
Series Volume: 12649
Publisher: Springer
Divisions: 20 Department of Computer Science
20 Department of Computer Science > Software Engineering
Event Title: 24th International Conference of the European Joint Conferences on Theory and Practice of Software
Event Location: virtual Conference
Event Dates: 27.03.-01.04.2021
Date Deposited: 20 Jul 2022 07:07
DOI: 10.1007/978-3-030-71500-7\_2
PPN:
Export:
Suche nach Titel in: TUfind oder in Google
Send an inquiry Send an inquiry

Options (only for editors)
Show editorial Details Show editorial Details