Inferring Loop Invariants Using Postconditions
From MaRDI portal
Publication:3586008
Abstract: One of the obstacles in automatic program proving is to obtain suitable loop invariants. The invariant of a loop is a weakened form of its postcondition (the loop's goal, also known as its contract); the present work takes advantage of this observation by using the postcondition as the basis for invariant inference, using various heuristics such as "uncoupling" which prove useful in many important algorithms. Thanks to these heuristics, the technique is able to infer invariants for a large variety of loop examples. We present the theory behind the technique, its implementation (freely available for download and currently relying on Microsoft Research's Boogie tool), and the results obtained.
Recommendations
- Automatically inferring loop invariants via algorithmic learning
- Mechanical inference of invariants for FOR-loops
- Loop verification with invariants and contracts
- Verification of a class of loop programs without using loop invariants
- Programming Languages and Systems
- Elimination of loop invariants in program verification
- Ilinva: using abduction to generate loop invariants
- An iterative method for generating loop invariants
Cites work
- scientific article; zbMATH DE number 1693447 (Why is no real title available?)
- scientific article; zbMATH DE number 3740740 (Why is no real title available?)
- scientific article; zbMATH DE number 3574936 (Why is no real title available?)
- scientific article; zbMATH DE number 605806 (Why is no real title available?)
- scientific article; zbMATH DE number 1105469 (Why is no real title available?)
- scientific article; zbMATH DE number 1953274 (Why is no real title available?)
- scientific article; zbMATH DE number 5194318 (Why is no real title available?)
- Affine relationships among variables of a program
- Automatic Verification of Integer Array Programs
- Computer Aided Verification
- Generating all polynomial invariants in simple loops
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Invariant Synthesis for Combined Theories
- Invariant and type inference for matrices
- Model Checking Software
- Non-linear loop invariant generation using Gröbner bases
- Touch of class. Learning to program well with objects and contracts
- Verification of non-functional programs using interpretations in type theory
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
Cited in
(14)- On invariant checking
- On proving that an unsafe controller is not proven safe
- A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows
- Automatically inferring loop invariants via algorithmic learning
- Invariant relations for affine loops
- An extension of lazy abstraction with interpolation for programs with arrays
- A versatile concept for the analysis of loops
- Mechanical inference of invariants for FOR-loops
- Loop invariants: analysis, classification, and examples
- Loop verification with invariants and contracts
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- Automatic proving or disproving equality loop invariants based on finite difference techniques
- Precondition inference from intermittent assertions and application to contracts on collections
- Computing Preconditions and Postconditions of While Loops
Describes a project that uses
Uses Software
This page was built for publication: Inferring Loop Invariants Using Postconditions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3586008)
