• FOCI

  • Referenced in 58 articles [sw12868]
  • FOCI: and interpolating prover. FOCI is a decision procedure for quantifier-free first-order formulas ... importantly, it can compute quantifier-free Craig interpolants for inconsistent pairs (or more generally, sequences...
  • MathSAT

  • Referenced in 56 articles [sw09449]
  • computation of unsatisfiable cores and Craig interpolants (for abstraction refinement...
  • SMTInterpol

  • Referenced in 18 articles [sw07406]
  • Solver that can compute Craig interpolants for various theories. The solver is developed...
  • Wolverine

  • Referenced in 12 articles [sw14483]
  • Wolverine: battling bugs with interpolants. Wolverine is a software verifier that checks safety properties ... ANSI-C and C++ programs, deploying Craig interpolation to derive program invariants. We describe...
  • SLAB

  • Referenced in 8 articles [sw09875]
  • that interleaves automatic abstraction refinement using Craig interpolation with slicing, which removes irrelevant states...
  • eVolCheck

  • Referenced in 6 articles [sw09711]
  • program functions, function summaries, derived using Craig interpolation. In each check, the function summaries...
  • Ultimate Kojak

  • Referenced in 4 articles [sw23308]
  • based on CEGAR and Craig interpolation. The basic algorithm, described in an earlier work...
  • ANSYS

  • Referenced in 643 articles [sw00044]
  • ANSYS offers a comprehensive software suite that spans...
  • HSL

  • Referenced in 265 articles [sw00418]
  • HSL (formerly the Harwell Subroutine Library) is a...
  • LSQR

  • Referenced in 343 articles [sw00530]
  • Algorithm 583: LSQR: Sparse Linear Equations and Least...
  • Matlab

  • Referenced in 11496 articles [sw00558]
  • MATLAB® is a high-level language and interactive...
  • MiniSat

  • Referenced in 521 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...
  • PARI/GP

  • Referenced in 564 articles [sw00680]
  • PARI/GP is a widely used Computer Algebra System...
  • SLEPc

  • Referenced in 145 articles [sw00875]
  • SLEPc the Scalable Library for Eigenvalue Problem Computations...
  • ZEAL

  • Referenced in 15 articles [sw01033]
  • ZEAL is a general purpose package for computing...
  • PRISM

  • Referenced in 396 articles [sw01186]
  • PRISM: Probabilistic symbolic model checker. In this paper...
  • HySAT

  • Referenced in 23 articles [sw01980]
  • HySAT: An efficient proof engine for bounded model...