When Is a Formula a Loop Invariant?

DOI10.1007/978-3-319-23165-5_13zbMath1321.68191OpenAlexW2286020247MaRDI QIDQ2945711

Deepak Kapur, Stephan Falke

Publication date: 14 September 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Unnamed Item ⋮ On invariant synthesis for parametric systems

Cites Work

• Unnamed Item
• On invariant checking
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• Property-directed incremental invariant generation
• A refutational approach to geometry theorem proving
• Generating all polynomial invariants in simple loops
• Understanding IC3
• Generalized Property Directed Reachability
• SAT-Based Model Checking without Unrolling
• Verification Constraint Problems with Strengthening
• Linear Ranking for Linear Lasso Programs
• Property Directed Polyhedral Abstraction
• Ideals, Varieties, and Algorithms
• Model Checking Software
• Programming Languages and Systems
• Synthesis of Circular Compositional Program Proofs via Abduction

This page was built for publication: When Is a Formula a Loop Invariant?