Princess
From MaRDI portal
swMATH6872MaRDI QIDQ18941FDOQ18941
Author name not available (Why is that?)
Official website: http://www.philipp.ruemmer.org/princess.shtml
Cited In (47)
- 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
- FLATA
- bv2epr
- OpenSMT
- Eldarica
- HMC
- HSF
- SLAB
- SCOOT
- CSIsat
- Skeptik
- FOCI
- FunArray
- 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
- Lazy abstraction with interpolants for arrays
- c2i
- DDVerify
- EUREKA
- MoCHi
- LoAT
- RAHFT
- 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
