Loop invariants: analysis, classification, and examples

DOI10.1145/2506375MaRDI QIDQ5176169zbMATH OpenOpenAlexFDO

Authors Carlo A. Furia, Bertrand Meyer, Sergey Velder

Publication date 2 March 2015

Published in ACM Computing Surveys (Search for Journal in Brave)

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

zbMATH Keywords

formal verificationloop invariantsdeductive verificationpostconditionspreconditions

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Software verification has emerged as a key concern for ensuring the continued progress of information technology. Full verification generally requires, as a crucial step, equipping each loop with a "loop invariant". Beyond their role in verification, loop invariants help program understanding by providing fundamental insights into the nature of algorithms. In practice, finding sound and useful invariants remains a challenge. Fortunately, many invariants seem intuitively to exhibit a common flavor. Understanding these fundamental invariant patterns could therefore provide help for understanding and verifying a large variety of programs. We performed a systematic identification, validation, and classification of loop invariants over a range of fundamental algorithms from diverse areas of computer science. This article analyzes the patterns, as uncovered in this study, governing how invariants are derived from postconditions; it proposes a taxonomy of invariants according to these patterns, and presents its application to the algorithms reviewed. The discussion also shows the need for high-level specifications based on "domain theory". It describes how the invariants and the corresponding algorithms have been mechanically verified using an automated program prover; the proof source files are available. The contributions also include suggestions for invariant inference and for model-based specification.

Recommendations

• Automatic proving or disproving equality loop invariants based on finite difference techniques
• Mechanical inference of invariants for FOR-loops
• Theoretical Aspects of Computing - ICTAC 2004
• Elimination of loop invariants in program verification
• Predicate abstraction for software verification

Cites work

• scientific article; zbMATH DE number 3692621 (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 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1241849 (Why is no real title available?)
• scientific article; zbMATH DE number 610968 (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 2107164 (Why is no real title available?)
• scientific article; zbMATH DE number 5194318 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• Affine relationships among variables of a program
• Algorithms and Data Structures
• An axiomatic basis for computer programming
• An axiomatic proof technique for parallel programs
• Behavioral interface specification languages
• Computer Aided Verification
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• Grammar Analysis and Parsing by Abstract Interpretation
• Handbook of automated reasoning. In 2 vols
• Inferring Loop Invariants Using Postconditions
• Introduction to algorithms.
• Invariant Synthesis for Combined Theories
• Mathematical Theory Exploration
• Model Checking Software
• Modeling time in computing.
• Non-linear loop invariant generation using Gröbner bases
• Proof of correctness of data representations
• Proving the Correctness of Multiprocess Programs
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Verification: Theory and Practice

Cited in

(12)

• Loop Invariants from Counterexamples
• Pattern-based approach to automation of deductive verification of process-oriented programs: patterns, lemmas and algorithms
• A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows
• Fifty years of Hoare's logic
• Manifestation and Exploitation of Invariants in Bioinformatics
• The concept of class invariant in object-oriented programming
• Mechanical inference of invariants for FOR-loops
• Loop verification with invariants and contracts
• Loop invariants, exploration of regularities, and mathematical games
• Could We Have Chosen a Better Loop Invariant or Method Contract?
• Automatic proving or disproving equality loop invariants based on finite difference techniques
• Automated Technology for Verification and Analysis

Describes a project that uses

Uses Software

• ASTREE
• Z
• Boogie
• Eiffel

This page was built for publication: Loop invariants: analysis, classification, and examples

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5176169)