Inferring Loop Invariants Using Postconditions
From MaRDI portal
Publication:3586008
DOI10.1007/978-3-642-15025-8_15zbMATH Open1287.68108arXiv0909.0884OpenAlexW1788659055MaRDI QIDQ3586008FDOQ3586008
Authors: Carlo A. Furia, Bertrand Meyer 
Publication date: 3 September 2010
Published in: Fields of Logic and Computation (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/0909.0884
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
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Affine relationships among variables of a program
- Invariant and type inference for matrices
- Verification, Model Checking, and Abstract Interpretation
- Title not available (Why is that?)
- Title not available (Why is that?)
- Verification, Model Checking, and Abstract Interpretation
- Non-linear loop invariant generation using Gröbner bases
- Automatic Verification of Integer Array Programs
- Invariant Synthesis for Combined Theories
- Generating all polynomial invariants in simple loops
- Computer Aided Verification
- Verification of non-functional programs using interpretations in type theory
- Model Checking Software
- Touch of class. Learning to program well with objects and contracts
- 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
- Loop invariants: analysis, classification, and examples
- Mechanical inference of invariants for FOR-loops
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- Loop verification with invariants and contracts
- 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
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)
