Inferring Loop Invariants Using Postconditions

DOI10.1007/978-3-642-15025-8_15zbMath1287.68108arXiv0909.0884OpenAlexW1788659055MaRDI QIDQ3586008

Carlo A. Furia, Bertrand Meyer

Publication date: 3 September 2010

Published in: Fields of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/0909.0884

zbMATH Keywords

formal specificationscorrectness proofsloop invariantsassertion inference

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (6)

Loop verification with invariants and contracts ⋮ On proving that an unsafe controller is not proven safe ⋮ A versatile concept for the analysis of loops ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Loop invariants ⋮ Automatic proving or disproving equality loop invariants based on finite difference techniques

Uses Software

• HOL-Boogie
• KRAKATOA
• Eiffel
• Why3
• Caduceus
• ESC/Java
• Boogie
• Traffic 4
• ASTREE
• Houdini

Cites Work

• Affine relationships among variables of a program
• Generating all polynomial invariants in simple loops
• Non-linear loop invariant generation using Gröbner bases
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• Automatic Verification of Integer Array Programs
• Invariant and Type Inference for Matrices
• Verification of non-functional programs using interpretations in type theory
• Model Checking Software
• Invariant Synthesis for Combined Theories
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Inferring Loop Invariants Using Postconditions