Schematic Program Proofs with Abstract Execution

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 a...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2024-06, Vol.68 (2), p.7
Main Authors: Steinhöfel, Dominic, Hähnle, Reiner
Format: Article
Language:English
Subjects:
Automation
Cost analysis
Java
Verification
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-023-09692-0