CISPA
Browse
s10817-023-09692-0.pdf (2.6 MB)

Schematic Program Proofs with Abstract Execution

Download (2.6 MB)
journal contribution
posted on 2024-04-11, 07:55 authored by Dominic SteinhöfelDominic Steinhöfel, Reiner Hähnle
We propose Abstract Execution, a static verification framework based on symbolic execution and dynamic frames for proving properties of schematic programs. Since a schematic program may potentially represent infinitely many concrete programs, Abstract Execution can analyze infinitely many programs at once. Trading off expressiveness and automation, the framework allows proving many interesting (universal, behavioral) properties fully automatically. Its main application are correctness proofs of program transformations represented as pairs of schematic programs. We implemented Abstract Execution in a deductive verification framework and designed a graphical workbench supporting the modeling process. Abstract Execution has been applied to correct code refactoring, analysis of the cost impact of transformation rules, and parallelization of sequential code. Using our framework, we found and reported several bugs in the refactoring engines of the JAVA IDEs IntelliJ IDEA and Eclipse, which were acknowledged and fixed.

History

Primary Research Area

  • Threat Detection and Defenses

Journal

Journal of Automated Reasoning

Volume

68

Page Range

7-7

Publisher

Springer Nature

Open Access Type

  • Hybrid

Sub Type

  • Article

BibTeX

@article{Steinhöfel:Hähnle:2024, title = "Schematic Program Proofs with Abstract Execution", author = "Steinhöfel, Dominic" AND "Hähnle, Reiner", year = 2024, month = 6, journal = "Journal of Automated Reasoning", number = "2", pages = "7--7", publisher = "Springer Nature", issn = "0168-7433", doi = "10.1007/s10817-023-09692-0" }