• VeriMAP

  • Referenced in 11 articles [sw22866]
  • fields of constraint logic programming and SMT solving...
  • NLambda

  • Referenced in 7 articles [sw23172]
  • them, and an external satisfiability modulo theories (SMT) solver is regularly run by the interpreter ... more about the language in an article: ’SMT Solving for Functional Programming over Infinite Structures...
  • SAFARI

  • Referenced in 10 articles [sw28669]
  • SAFARI: SMT-Based Abstraction for Arrays with Interpolants. We present SAFARI, a model checker designed...
  • Ivy

  • Referenced in 10 articles [sw41668]
  • three modes: deductive verification using an SMT solver, abstraction and model checking, and manual proofs...
  • PySMT

  • Referenced in 5 articles [sw19843]
  • solver-agnostic library for fast prototyping of smt-based algorithms. pySMT: A library ... SMT formulae manipulation and solving http://www.pysmt.org. pySMT: a Python API for SMT: pySMT makes ... native solvers, or by wrapping any SMT-Lib complaint solver, Dump your problems ... SMT-Lib format, and more...
  • SIMPLY

  • Referenced in 5 articles [sw11807]
  • from a CSP modeling language to the SMT-LIB format. n this paper we introduce ... language for CSP modeling to the standard SMT-LIB format. The current version of Simply ... year-over-year increase in performance of SMT solvers, we hope that such a system ... compiler can also be used for easy SMT benchmark generation...
  • ASPMT2SMT

  • Referenced in 5 articles [sw13280]
  • System ASPMT2SMT: computing ASPMT theories by SMT solvers. Answer set programming modulo theories (ASPMT ... ASPMT programs can be turned into SMT instances, thereby allowing SMT solvers to compute stable ... system uses ASP grounder gringo and SMT solver z3. gringo partially grounds input programs while...
  • SMTtoTPTP

  • Referenced in 5 articles [sw13650]
  • converter from proof problems written in the SMT-LIB format into the TPTP TFF format ... SMT-LIB format supports polymorphic sorts and frequently used theories like those of uninterpreted function ... theories. SMTtoTPTP is useful for, e.g., making SMT-LIB problems available to TPTP system developers ... making TPTP systems available to users of SMT solvers. This paper describes how the conversion...
  • Z3-str

  • Referenced in 9 articles [sw19493]
  • extension of the Z3 SMT solver through its plug-in interface. Z3-str treats strings...
  • fzn2smt

  • Referenced in 4 articles [sw13501]
  • from the FlatZinc language to the standard SMT-LIB language version 1.2. SMT stands ... mind of help testing the adequacy of SMT technology outside the field of verification, where ... instances with state-of-the art SMT solvers, by taking profit of recent advances ... make sense in the context of SMT. Only the alldifferent and cumulative MiniZinc global constraints...
  • KRATOS

  • Referenced in 8 articles [sw07808]
  • MathSat, and uses state-of-the-art SMT-based techniques for program abstractions and refinements...
  • iProver-Eq

  • Referenced in 8 articles [sw09452]
  • state-of-the-art SMT solver. The first-order reasoning employs a saturation algorithm making...
  • Rex

  • Referenced in 8 articles [sw11888]
  • expression constraints. Rex is implemented using the SMT solver Z3, and we provide experimental evaluation...
  • PAGAI

  • Referenced in 8 articles [sw13095]
  • algorithms combining abstract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside...
  • Skew

  • Referenced in 8 articles [sw14905]
  • SMT: The Skew Mu Toolbox. This toolbox was written in colloboration with Gilles Ferreres...
  • HyComp

  • Referenced in 4 articles [sw20163]
  • HyComp: An SMT-based model checker for hybrid systems. HyComp is a model checker ... hybrid systems based on Satisfiability Modulo Theories (SMT). HyComp takes as input networks of hybrid ... transition system, which can be analyzed using SMT-based verification techniques (e.g. BMC, K-induction ... applying off-the-shelf algorithms based on SMT. We describe the tool in terms...
  • bv2epr

  • Referenced in 7 articles [sw07142]
  • many applications of satisfiability modulo theories (SMT). In recent years, efficient approaches for solving fixed...
  • TACO

  • Referenced in 7 articles [sw07668]
  • based on SAT-solving, model checking, or SMT-solving...
  • ERODE

  • Referenced in 7 articles [sw20210]
  • backend based on the well-known Z3 SMT solver to compute the coarsest equivalence that...
  • H-PILoT

  • Referenced in 7 articles [sw23305]
  • base theory. Specialized provers and standard SMT solvers can be used for testing the satisfiability...