swMATH12868MaRDI QIDQ24792FDOQ24792
Author name not available (Why is that?)
Official website: http://www.kenmcmil.com/foci.html
Cited In (90)
- Mind the gap: bit-vector interpolation recast over linear integer arithmetic
- Abstract Counterexamples for Non-disjunctive Abstractions
- Craig interpolation in the presence of unreliable connectives
- Efficient interpolant generation in satisfiability modulo linear integer arithmetic
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- Title not available (Why is that?)
- Rewriting interpolants
- Craig interpolation with clausal first-order tableaux
- Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
- Predicate generation for learning-based quantifier-free loop invariant inference
- Challenges in Constraint-Based Analysis of Hybrid Systems
- Interpolation and model checking for nonlinear arithmetic
- Latticed \(k\)-induction with an application to probabilistic programs
- Resolution proof transformation for compression and interpolation
- Competent predicate abstraction in model checking
- State of the Union: Type Inference Via Craig Interpolation
- Reasoning in the theory of heap: satisfiability and interpolation
- Interpolant Generation for UTVPI
- Ground Interpolation for Combined Theories
- Interpolation and Symbol Elimination
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs
- Preface: Special issue on interpolation
- Proof tree preserving tree interpolation
- Interpolation systems for ground proofs in automated deduction: a survey
- Craig interpolation in the presence of non-linear constraints
- Interpolation and model checking
- Parallelizing SMT solving: lazy decomposition and conciliation
- Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
- SAT-based verification for timed component connectors
- SAT-based verification for timed component connectors
- Quantifier-free interpolation in combinations of equality interpolating theories
- A Tutorial on Satisfiability Modulo Theories
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- An institution-independent proof of the Robinson consistency theorem
- Experience of improving the BLAST static verification tool
- Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
- Complete instantiation-based interpolation
- Unbounded model-checking with interpolation for regular language constraints
- Interpolation in computing science: The semantics of modularization
- Constraint solving for interpolation
- Beaver
- Cogent
- BLAST
- SIMPLIFY
- Princess
- bv2epr
- E-SETHEO
- SMTInterpol
- PeRIPLO
- OpenSMT
- eVolCheck
- SLAB
- SCOOT
- CSIsat
- AMUSE
- CMU Benchmarks
- MUP
- SATLIB Benchmark Suite
- Skeptik
- Equality detection for linear arithmetic constraints
- SatAbs
- PAGAI
- Wolverine
- Beyond quantifier-free interpolation in extensions of Presburger arithmetic
- On interpolation in decision procedures
- A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints
- JavaSMT
- DDVerify
- Zapato
- DPT
- SAT-Based Model Checking
- A survey of satisfiability modulo theory
- Satisfiability modulo theories
- Constrained monotonic abstraction: a CEGAR for parameterized verification
- Preservation of Craig interpolation by the product of matrix logics
- KoAT
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- On interpolation in automated theorem proving
- QuickFOIL
- An interpolating theorem prover
- Gene sorting in differential evolution with cross-generation mutation
- Ground interpolation for the theory of equality
- Quantifier-free interpolation of a theory of arrays
- Tools and Algorithms for the Construction and Analysis of Systems
- Improved single pass algorithms for resolution proof reduction
- Interpolants for Linear Arithmetic in SMT
- Ground Interpolation for the Theory of Equality
This page was built for software: FOCI
