• Equinox

  • Referenced in 2 articles [sw09768]
  • anatomy of Equinox -- an extensible automated reasoning tool for first-order logic and beyond. Equinox ... automated reasoning tool for first-order logic. It is also a framework for building highly ... targeted automated reasoning tools for specific domains.par The aim behind Equinox is to obtain ... automated reasoning tool with a modular and extensible architecture. SAT modulo theory (SMT) solvers have...
  • TPS

  • Referenced in 67 articles [sw00973]
  • proving include hardware and software verification, partial automation of various mathematical activities, promoting development ... these disciplines, expert systems which can reason, and certain aspects of artificial intelligence...
  • Jakarta

  • Referenced in 18 articles [sw01269]
  • JaKarTa is a toolset for specifying and reasoning about the JavaCard platform. The main ingredients ... assistants; the JaKarTa Automation Kit (JAK), a toolset to support reasoning about executable specifications within...
  • TacticToe

  • Referenced in 3 articles [sw28627]
  • combining machine learning with translation to automated reasoning have recently become an important component ... hammer” tech- niques complement traditional proof assistant automation as implemented by tactics and decision procedures...
  • IsaFoL

  • Referenced in 3 articles [sw19193]
  • methodology for formalizing modern research in automated reasoning. Our initial focus is on well-established...
  • Valigator

  • Referenced in 3 articles [sw00994]
  • that efficiently combines symbolic computation and automated reasoning in a uniform framework. The system offers...
  • EPGY

  • Referenced in 3 articles [sw28722]
  • system uses a combination of automated reasoning and symbolic computation to verify individual proof steps...
  • MATHsAiD

  • Referenced in 3 articles [sw21355]
  • Discovery Tool. In the field of automated reasoning, one of the most challenging (even...
  • Aximo

  • Referenced in 4 articles [sw15031]
  • Aximo: Automated Axiomatic Reasoning for Information Update. Aximo is a software written in C++ that...
  • Viper

  • Referenced in 4 articles [sw15038]
  • verification infrastructure for permission-based reasoning. The automation of verification techniques based on first-order ... allowing the developers of higher-level reasoning techniques to focus their efforts at an appropriate...
  • FORMULA 2.0

  • Referenced in 2 articles [sw13248]
  • domain-specific abstractions and compilers, (2) efficient reasoning and compilation of input programs, (3) diverse ... easily express rich synthesis / verification problems. Automated reasoning is enabled by efficient symbolic execution...
  • GROVER

  • Referenced in 2 articles [sw09968]
  • meaning. Through the development of an automated reasoning system, called &/GROVER, we have tried...
  • Caper

  • Referenced in 2 articles [sw20269]
  • present Caper, a prototype tool for automated reasoning in such a logic. Caper is based...
  • jSMTLIB

  • Referenced in 2 articles [sw19842]
  • response requirements for Satisfiability-Modulo-Theories automated reasoning tools. The standard has been an incentive...
  • HOARD ATINF

  • Referenced in 2 articles [sw28890]
  • prototype) is called HOARDATINF (Human Oriented Automated Reasoning on your Desk) and has been specialized...
  • Logtk

  • Referenced in 1 article [sw28635]
  • Logtk : A Logic ToolKit for Automated Reasoning and its Implementation. We describe the design ... Logtk, an OCaml library for writing automated reasoning tools that deal with (possibly typed) first...
  • MUNCH

  • Referenced in 1 article [sw07181]
  • MUNCH -- automated reasoner for sets and multisets This system description provides an overview ... MUNCH reasoner for sets and multisets. MUNCH takes as the input a formula ... MUNCH is the first fully automated reasoner for this logic. MUNCH reduces input formulas...
  • EasyCrypt

  • Referenced in 23 articles [sw09738]
  • using off-the-shelf SMT solvers and automated theorem provers, and then compiled into verifiable ... CertiCrypt framework. The tool supports most common reasoning patterns and is significantly easier...
  • LEO-II

  • Referenced in 42 articles [sw00512]
  • winner of the THF division (automation of higher-order logic) at CASC-J5. At CASC ... order divisions FOF and CNF and performed reasonably well. LEO-II has been the first...
  • ManyOpt

  • Referenced in 1 article [sw18803]
  • current solvers have limited ability for deductive reasoning or the use of domain-specific theories ... integrality constraints does not yet exploit automated reasoning tools such as SMT solvers. This seems...