FOCI
From MaRDI portal
Software:24792
No author found.
Related Items (63)
Ground interpolation for the theory of equality ⋮ Quantifier-Free Interpolation of a Theory of Arrays ⋮ Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic ⋮ Preface: Special issue on interpolation ⋮ Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Proof tree preserving tree interpolation ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Interpolation and model checking for nonlinear arithmetic ⋮ Latticed \(k\)-induction with an application to probabilistic programs ⋮ Unnamed Item ⋮ Craig Interpolation in the Presence of Non-linear Constraints ⋮ A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints ⋮ SAT-Based Model Checking ⋮ Satisfiability Modulo Theories ⋮ Interpolation and Model Checking ⋮ Unbounded Model-Checking with Interpolation for Regular Language Constraints ⋮ An institution-independent proof of the Robinson consistency theorem ⋮ Constraint solving for interpolation ⋮ Craig interpolation with clausal first-order tableaux ⋮ Equality detection for linear arithmetic constraints ⋮ SAT-based verification for timed component connectors ⋮ An interpolating sequent calculus for quantifier-free Presburger arithmetic ⋮ Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions ⋮ Unnamed Item ⋮ Complete instantiation-based interpolation ⋮ Preservation of Craig interpolation by the product of matrix logics ⋮ Interpolants for Linear Arithmetic in SMT ⋮ Resolution proof transformation for compression and interpolation ⋮ On Interpolation in Decision Procedures ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Improved Single Pass Algorithms for Resolution Proof Reduction ⋮ Quantifier-free interpolation in combinations of equality interpolating theories ⋮ Rewriting Interpolants ⋮ Experience of improving the BLAST static verification tool ⋮ Craig interpolation in the presence of unreliable connectives ⋮ Competent predicate abstraction in model checking ⋮ Gene sorting in differential evolution with cross-generation mutation ⋮ Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification ⋮ A Tutorial on Satisfiability Modulo Theories ⋮ Interpolant Generation for UTVPI ⋮ Ground Interpolation for Combined Theories ⋮ Interpolation and Symbol Elimination ⋮ Challenges in Constraint-Based Analysis of Hybrid Systems ⋮ State of the Union: Type Inference Via Craig Interpolation ⋮ Ground Interpolation for the Theory of Equality ⋮ Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic ⋮ Efficient Interpolant Generation in Satisfiability Modulo Theories ⋮ Quantified Invariant Generation Using an Interpolating Saturation Prover ⋮ Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic ⋮ Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic ⋮ Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference ⋮ Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference ⋮ Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF ⋮ On Interpolation and Symbol Elimination in Theory Extensions ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic ⋮ Interpolation in computing science: The semantics of modularization ⋮ A Survey of Satisfiability Modulo Theory ⋮ Abstract Counterexamples for Non-disjunctive Abstractions ⋮ Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations ⋮ Tools and Algorithms for the Construction and Analysis of Systems ⋮ An interpolating theorem prover ⋮ On interpolation in automated theorem proving ⋮ Reasoning in the theory of heap: satisfiability and interpolation
This page was built for software: FOCI