Boosting k-Induction with Continuously-Refined Invariants
No abstract available.
Related papers
- ICE-Based Refinement Type Discovery for Higher-Order Functional Programs TACAS 2018
- Ivy: safety verification by interactive generalization PLDI 2016
- Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis SAS 2020
- Abstraction Refinement-Guided Program Synthesis for Robot Learning from Demonstrations OOPSLA 2025
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays TACAS 2021
- A Refinement Methodology for Distributed Programs in Rust OOPSLA 2025
- Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants CAV 2005
- Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction SAS 2018