This seminar studies topics from our research area incremental verification. Techniques in incremental verification are a key enabler for applying formal verification in modern software project. To deal with dozens of rapid changes, incremental verification techniques aim at a more efficient reverification of a modified program. For this purpose, incremental verification reuses information of a previous verification run. The kind of information and its use distinguish the different approaches. In this seminar, we look at four different classes of incremental verification: functional equivalence checking, reuse of intermediate results, proof adaption, and skipped verification.
In functional equivalence checking, it is verified that modified program parts show the same input/output behavior as the part before the verification.
Techniques reusing intermediate results avoid reexploration of known results, e.g., invariants, satisfiability results, or abstraction level. Their assumption is that a large portion of the intermediate results is still valid and needed for the verification of the modified program.
Approaches for proof adaption check which proof parts remain valid and perform a verification step for invalid proof parts.
The fourth class skipped verification is related to the class of proof adaption. Techniques in this class stop verification as soon as modification can be reached or perform a lightweight verification as long as no modification has been reached.
Functional Equivalence Checking
- Regression Verification
Benny Godlin, Ofer Strichman: . DAC 2009 Regression verification
- Relation Regression Verification
Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, Mattias Ulbrich: . ASE 2014 Automating regression verification
David A. Ramos, Dawson R. Engler: . CAV 2011 Practical, Low-Effort Equivalence Verification of Real Code
Reusing Intermediate Results
- Constraints Reuse
Willem Visser, Jaco Geldenhuys, Matthew B. Dwyer: . FSE 2012 Green: reducing, reusing and recycling constraints in program analysis
- Precision Reuse
Dirk Beyer, Stefan Löwe, Evgeny Novikov, Andreas Stahlbauer, Philipp Wendler: . ESEC/SIGSOFT FSE 2013 Precision reuse for efficient regression verification
- Reusing Trace Abstractions
Bat-Chen Rothenberg, Daniel Dietsch, Matthias Heizmann: . SAS 2018 Incremental Verification Using Trace Abstraction
- Incremental Upgrade Checking
Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina: . FMCAD 2012 Incremental upgrade checking by means of interpolation-based function summaries
- Extreme Model Checking
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Marco A. A. Sanvido: . Verification: Theory and Practice 2003 Extreme Model Checking
- Directed Incremental Verification
Suzette Person, Guowei Yang, Neha Rungta, Sarfraz Khurshid: . PLDI 2011 Directed incremental symbolic execution
- Memoized Symbolic Execution
Guowei Yang, Corina S. Pasareanu, Sarfraz Khurshid: . ISSTA 2012 Memoized symbolic execution
- Regression Model Checking
Guowei Yang, Matthew B. Dwyer, Gregg Rothermel: . ICSM 2009 Regression model checking
Ahmet Çelik, Karl Palmskog, Milos Gligoric:. ASE 2017 iCoq: regression proof selection for large-scale verification projects
Wenxi Wang, Kaiyuan Wang, Milos Gligoric, Sarfraz Khurshid: . TACAS 2019 Incremental Analysis of Evolving Alloy Models