CISPA
Browse
- No file added yet -

Certified Abstract Cost Analysis

Download (507.87 kB)
conference contribution
posted on 2023-11-29, 18:17 authored by Elvira Albert, Reiner Hähnle, Alicia Merayo, Dominic Steinhöfel
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.

History

Preferred Citation

Elvira Albert, Reiner Hähnle, Alicia Merayo and Dominic Steinhöfel. Certified Abstract Cost Analysis. In: Fundamental Approaches to Software Engineering (FASE). 2021.

Primary Research Area

  • Empirical and Behavioral Security

Name of Conference

Fundamental Approaches to Software Engineering (FASE)

Legacy Posted Date

2021-10-19

Open Access Type

  • Hybrid

BibTeX

@inproceedings{cispa_all_3510, title = "Certified Abstract Cost Analysis", author = "Albert, Elvira and Hähnle, Reiner and Merayo, Alicia and Steinhöfel, Dominic", booktitle="{Fundamental Approaches to Software Engineering (FASE)}", year="2021", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC