• EFSMT

  • Referenced in 2 articles [sw19487]
  • exists-forall quantified first-order fragment of propositional combinations over constraints (including nonlinear arithmetic ... solvers for respectively solving universally and existentially quantified problems. This algorithms builds on commonly used ... generalizes them to quantifier reasoning by counterexample-guided constraint strengthening. The EFSMT solver uses Bernstein...
  • foxPSL

  • Referenced in 2 articles [sw13725]
  • with a class system and existential quantifiers, allowing for efficient grounding. Moreover, it implements ... configurable optimizations, like optimized grounding of constraints and lazy inference, that improve grounding and inference...
  • INTBIS

  • Referenced in 31 articles [sw00442]
  • Algorithm 681: INTBIS, a portable interval Newton/bisection package...
  • TPTP

  • Referenced in 401 articles [sw04143]
  • The TPTP (Thousands of Problems for Theorem Provers...
  • REDLOG

  • Referenced in 166 articles [sw04250]
  • REDLOG is a package that extends the computer...
  • RealPaver

  • Referenced in 51 articles [sw04401]
  • Algorithm 852 Realpaver: nonlinear constraint solving & rigorous global...
  • CUDD

  • Referenced in 158 articles [sw04446]
  • The CUDD package provides functions to manipulate Binary...
  • z3

  • Referenced in 606 articles [sw04887]
  • Z3 is a high-performance theorem prover being...
  • SIMPLIFY

  • Referenced in 141 articles [sw04976]
  • Extended static checking. This paper provides an overview...
  • gaol

  • Referenced in 14 articles [sw05586]
  • Gaol: NOT Just Another Interval Library project (”gaol...
  • MONA

  • Referenced in 135 articles [sw06170]
  • MONA implementation secrets. The MONA tool provides an...
  • FINDER

  • Referenced in 40 articles [sw06376]
  • Finite domain enumerator. This is a finite domain...
  • SATCHMO

  • Referenced in 97 articles [sw06619]
  • SATCHMO: a theorem prover implemented in Prolog. The...
  • ESC/Java

  • Referenced in 137 articles [sw07217]
  • The Extended Static Checker for Java version 2...
  • AQCS

  • Referenced in 15 articles [sw08109]
  • Approximate quantified constraint solving (AQCS). AQCS is a...
  • Ivy

  • Referenced in 39 articles [sw10279]
  • Ivy: A Preprocessor and Proof Checker for First...
  • IbexOpt

  • Referenced in 14 articles [sw12331]
  • Exploiting monotonicity in interval constraint propagation. ...
  • Datalog

  • Referenced in 293 articles [sw20023]
  • Datalog is a declarative logic programming language that...
  • Numerica

  • Referenced in 46 articles [sw21227]
  • Numerica: A modeling language for global optimization. Many...
  • Ivy

  • Referenced in 10 articles [sw41668]
  • Ivy: A Multi-modal Verification Tool for Distributed...