An Interpolating Theorem Prover
No abstract available.
Related papers
- Quantified Invariant Generation Using an Interpolating Saturation Prover TACAS 2008
- Dependent types from counterexamples POPL 2010
- The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover CAV 2006
- AVATAR: The Architecture for First-Order Theorem Provers CAV 2014
- A Generic Theorem Prover of CSP Refinement TACAS 2005
- A Generic Cyclic Theorem Prover APLAS 2012
- Formalizing a JVML Verifier for Initialization in a Theorem Prover CAV 2001
- Using a Theorem Prover for Reasoning about Concurrent Algorithms CAV 1992