Princess

swMATH6872MaRDI QIDQ18941FDOQ18941

Author name not available (Why is that?)

Cited In (28)

• ICE-based refinement type discovery for higher-order functional programs
• Reasoning in the theory of heap: satisfiability and interpolation
• Preface: Special issue on interpolation
• Proof tree preserving tree interpolation
• Interpolation systems for ground proofs in automated deduction: a survey
• Interpolation and model checking
• Parallelizing SMT solving: lazy decomposition and conciliation
• Rewriting-based quantifier-free interpolation for a theory of arrays
• Quantifier-free interpolation in combinations of equality interpolating theories
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• An extension of lazy abstraction with interpolation for programs with arrays
• A calculus for modular loop acceleration
• Guiding Craig interpolation with domain-specific abstractions
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
• On recursion-free Horn clauses and Craig interpolation
• Complete instantiation-based interpolation
• Efficient interpolant generation in satisfiability modulo linear integer arithmetic
• 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
• Lazy abstraction with interpolants for arrays
• SAT-Based Model Checking
• Craig interpolation with clausal first-order tableaux
• Solving non-linear Horn clauses using a linear Horn clause solver
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Learning inductive invariants by sampling from frequency distributions
• Quantifier-free interpolation of a theory of arrays

This page was built for software: Princess