Mechanical inference of invariants for FOR-loops

DOI10.1016/J.JSC.2008.11.008zbMATH Open1208.68147OpenAlexW2035919470MaRDI QIDQ604381FDOQ604381

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

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

zbMATH Keywords

mechanical verificationFOR-loopmechanical inference of loop invariantsRCPV

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• The synthesis of loop predicates
• An axiomatic basis for computer programming
• Computing polynomial program invariants
• Title not available (Why is that?)
• Programming as a Discipline of Mathematical Nature
• Logical analysis of programs
• Predicate abstraction for software verification
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• A note on a standard strategy for developing loop invariants and loops
• Strongest invariant functions: Their use in the systematic analysis of while statements
• Generating algebraic laws from imperative programs
• 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
• Title not available (Why is that?)
• Subgoal induction
• Some Aspects of the Verification of Loop Computations
• Title not available (Why is that?)
• A note on the for statement

Cited In (5)

• Inferring Loop Invariants Using Postconditions
• Generalizing specifications for uniformly implemented loops
• Automatically inferring loop invariants via algorithmic learning
• Elimination of loop invariants in program verification
• Loop Invariants from Counterexamples

Uses Software

• Boogie
• KeY

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)