FOCI

swMATH12868MaRDI QIDQ24792FDOQ24792

Author name not available (Why is that?)

Cited In (63)

• Mind the gap: bit-vector interpolation recast over linear integer arithmetic
• Abstract Counterexamples for Non-disjunctive Abstractions
• Title not available (Why is that?)
• Rewriting interpolants
• 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
• On interpolation and symbol elimination in theory extensions
• Complete instantiation-based interpolation
• Unbounded model-checking with interpolation for regular language constraints
• Craig interpolation in the presence of unreliable connectives
• Efficient interpolant generation in satisfiability modulo linear integer arithmetic
• Interpolation in computing science: The semantics of modularization
• Constraint solving for interpolation
• Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
• Equality detection for linear arithmetic constraints
• 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
• SAT-Based Model Checking
• A survey of satisfiability modulo theory
• Satisfiability modulo theories
• Craig interpolation with clausal first-order tableaux
• Constrained monotonic abstraction: a CEGAR for parameterized verification
• Preservation of Craig interpolation by the product of matrix logics
• Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
• On interpolation in automated theorem proving
• 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