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.


Primary Research Area

  • Threat Detection and Defenses


Journal of Automated Reasoning



Page Range



Springer Nature

Open Access Type

  • Hybrid

Sub Type

  • Article


@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" }