Mechanical inference of invariants for FOR-loops

DOI10.1016/J.JSC.2008.11.008MaRDI QIDQ604381zbMATH OpenOpenAlexFDO

Authors Stefan Kauer, Jürgen F. H. Winkler

Publication date 10 November 2010

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jsc.2008.11.008

zbMATH Keywords

mechanical verificationFOR-loopmechanical inference of loop invariantsRCPV

Mathematics Subject Classification ID

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

Recommendations

• On the mechanical derivation of loop invariants
• Automatically inferring loop invariants via algorithmic learning
• Inferring Loop Invariants Using Postconditions
• Synthesizing invariants by solving solvable loops
• Loop invariants: analysis, classification, and examples

Cites work

• scientific article; zbMATH DE number 107605 (Why is no real title available?)
• scientific article; zbMATH DE number 1031980 (Why is no real title available?)
• scientific article; zbMATH DE number 194543 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• A Heuristic for Deriving Loop Functions
• A Note on Synthesis of Inductive Assertions
• A note on a standard strategy for developing loop invariants and loops
• A note on the for statement
• ADI: Automatic Derivation of Invariants
• An axiomatic basis for computer programming
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• Computing polynomial program invariants
• Generating algebraic laws from imperative programs
• Logical analysis of programs
• Predicate abstraction for software verification
• Programming as a Discipline of Mathematical Nature
• Some Aspects of the Verification of Loop Computations
• Strongest invariant functions: Their use in the systematic analysis of while statements
• Subgoal induction
• The Determination of Loop Invariants for Programs with Arrays
• The synthesis of loop predicates

Cited in

(9)

• On invariant checking
• Loop Invariants from Counterexamples
• Inferring Loop Invariants Using Postconditions
• Generalizing specifications for uniformly implemented loops
• Automating Verification of Loops by Parallelization
• Automatically inferring loop invariants via algorithmic learning
• Loop invariants: analysis, classification, and examples
• Loop verification with invariants and contracts
• Elimination of loop invariants in program verification

Describes a project that uses

Uses Software

• KeY
• Boogie

This page was built for publication: Mechanical inference of invariants for FOR-loops

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