On Extending Bounded Proofs to Inductive Proofs
No abstract available.
Related papers
- Property Directed Reachability with Extended Resolution CAV 2025
- Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A) CAV 2003
- Automatic cyclic termination proofs for recursive procedures in separation logic CPP 2017
- Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions POPL 2026
- Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings POPL 2025
- Accelerating Syntax-Guided Invariant Synthesis TACAS 2018
- Bounded Sort Polymorphism with Elimination Constraints POPL 2026
- (Deep) induction rules for GADTs CPP 2022