Albert, Elvira ; Hähnle, Reiner ; Merayo, Alicia ; Steinhöfel, Dominic
Hrsg.: Guerra, Esther ; Stoelinga, Marielle (2021)
Certified Abstract Cost Analysis.
24th International Conference of the European Joint Conferences on Theory and Practice of Software. virtual Conference (27.03.2021-01.04.2021)
doi: 10.1007/978-3-030-71500-7_2
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (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.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2021 |
| Herausgeber: | Guerra, Esther ; Stoelinga, Marielle |
| Autor(en): | Albert, Elvira ; Hähnle, Reiner ; Merayo, Alicia ; Steinhöfel, Dominic |
| Art des Eintrags: | Bibliographie |
| Titel: | Certified Abstract Cost Analysis |
| Sprache: | Englisch |
| Publikationsjahr: | 20 März 2021 |
| Verlag: | Springer |
| Buchtitel: | Fundamental Approaches to Software Engineering |
| Reihe: | Lecture Notes in Computer Science |
| Band einer Reihe: | 12649 |
| Veranstaltungstitel: | 24th International Conference of the European Joint Conferences on Theory and Practice of Software |
| Veranstaltungsort: | virtual Conference |
| Veranstaltungsdatum: | 27.03.2021-01.04.2021 |
| DOI: | 10.1007/978-3-030-71500-7_2 |
| URL / URN: | https://link.springer.com/chapter/10.1007/978-3-030-71500-7_... |
| Kurzbeschreibung (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. |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Software Engineering |
| Hinterlegungsdatum: | 20 Jul 2022 07:07 |
| Letzte Änderung: | 09 Jan 2023 08:26 |
| PPN: | 50341882X |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum