Refinement and Term Synthesis in Loop Invariant Generation

10.29007/5wpt ◽  
2018 ◽  
Author(s):  
Ewen Maclean ◽  
Andrew Ireland ◽  
Lucas Dixon ◽  
Robert Atkey
Keyword(s):  
Program Analysis ◽  
Loop Invariant ◽  
Proof Planning ◽  
Invariant Generation ◽  
Correctness Proofs ◽  
Complex Problems

We present a technique for refining incorrect or insufficiently strong loop invariants in correctness proofs for imperative programs. We rely on previous work [16] in combining program analysis and Proof Planning, and exploit IsaPlanner’s use of meta-variables and goal-naming to generate correct loop invariants. We present a simple example in detail and show how this scales to more complex problems.

Decidability of affine solution problems

2019 ◽  
Vol 30 (3) ◽  
pp. 697-714
Author(s):  
Stefan Hetzl ◽  
Sebastian Zivota
Keyword(s):  
Computer Science ◽  
Iteration Procedure ◽  
Loop Invariant ◽  
Affine Spaces ◽  
Invariant Generation ◽  
First Order ◽  
Equivalent Statement

Abstract We present formula equations—first-order formulas with unknowns standing for predicates—as a general formalism for treating certain questions in logic and computer science, like the Auflösungsproblem and loop invariant generation. In the case of the language of affine terms over $\mathbb{Q}$, we translate a quantifier-free formula equation into an equivalent statement about affine spaces over $\mathbb{Q}$, which can then be decided by an iteration procedure.

scholarly journals CoVEGI: Cooperative Verification via Externally Generated Invariants

2021 ◽  
pp. 108-129
Author(s):  
Jan Haltermann ◽  
Heike Wehrheim
Keyword(s):  
Software Verification ◽  
Black Box ◽  
Loop Invariant ◽  
Invariant Generation ◽  
Smt Solving ◽  
The Core ◽  
Verification Tool ◽  
Verification Methods ◽  
Speed Up ◽  
Verification Tools

AbstractSoftware verification has recently made enormous progress due to the development of novel verification methods and the speed-up of supporting technologies like SMT solving. To keep software verification tools up to date with these advances, tool developers keep on integrating newly designed methods into their tools, almost exclusively by re-implementing the method within their own framework. While this allows for a conceptual re-use of methods, it nevertheless requires novel implementations for every new technique.In this paper, we employ cooperative verification in order to avoid re-implementation and enable usage of novel tools as black-box components in verification. Specifically, cooperation is employed for the core ingredient of software verification which is invariant generation. Finding an adequate loop invariant is key to the success of a verification run. Our framework named CoVEGI allows a master verification tool to delegate the task of invariant generation to one or several specialized helper invariant generators. Their results are then utilized within the verification run of the master verifier, allowing in particular for crosschecking the validity of the invariant. We experimentally evaluate our framework on an instance with two masters and three different invariant generators using a number of benchmarks from SV-COMP 2020. The experiments show that the use of CoVEGI can increase the number of correctly verified tasks without increasing the used resources.

scholarly journals Non-linear loop invariant generation using Gröbner bases

2004 ◽  
Vol 39 (1) ◽  
pp. 318-329 ◽  
Author(s):  
Sriram Sankaranarayanan ◽  
Henny B. Sipma ◽  
Zohar Manna
Keyword(s):  
Gröbner Bases ◽  
Grobner Bases ◽  
Loop Invariant ◽  
Invariant Generation ◽  
Non Linear
Sign in / Sign up

Export Citation Format

Share Document