Loop Invariants from Counterexamples

DOI10.1007/978-3-319-66706-5_7zbMATH Open1420.68128OpenAlexW2750327884MaRDI QIDQ5233241FDOQ5233241

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

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

Mathematics Subject Classification ID

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

Cited In (2)

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

Uses Software

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

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)