Mechanical inference of invariants for FOR-loops

DOI10.1016/j.jsc.2008.11.008zbMath1208.68147OpenAlexW2035919470MaRDI QIDQ604381

Jürgen F. H. Winkler, Stefan Kauer

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)

Uses Software

• Boogie
• KeY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Strongest invariant functions: Their use in the systematic analysis of while statements
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• A note on a standard strategy for developing loop invariants and loops
• Generating algebraic laws from imperative programs
• Computing polynomial program invariants
• A Heuristic for Deriving Loop Functions
• A Note on Synthesis of Inductive Assertions
• ADI: Automatic Derivation of Invariants
• The Determination of Loop Invariants for Programs with Arrays
• Subgoal induction
• Logical analysis of programs
• Some Aspects of the Verification of Loop Computations
• Programming as a Discipline of Mathematical Nature
• Predicate abstraction for software verification
• The synthesis of loop predicates
• An axiomatic basis for computer programming
• A note on the for statement

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