Loop Invariants from Counterexamples

DOI10.1007/978-3-319-66706-5_7MaRDI QIDQ5233241zbMATH OpenOpenAlexFDO

Authors Marius Greitschus, Daniel Dietsch, Andreas Podelski

Publication date 16 September 2019

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-66706-5_7

Mathematics Subject Classification ID

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

Recommendations

• Loop invariants: analysis, classification, and examples
• Programming Languages and Systems
• An iterative method for generating loop invariants
• Inadequacy of computable loop invariants
• Synthesizing invariants by solving solvable loops
• Loops with the weak inverse property
• Solving invariant generation for unsolvable loops
• Mechanical inference of invariants for FOR-loops
• Reasoning about loops in total and general correctness

Cited in

(2)

• The map equality domain
• Under-approximating loops in C programs for fast counterexample detection

Describes a project that uses

Uses Software

• Ultimate
• UFO
• CVC4
• CPAchecker
• SMTInterpol
• z3
• SLAM

This page was built for publication: Loop Invariants from Counterexamples

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