• ASTREE

  • Referenced in 115 articles [sw13704]
  • based static program analyzer aiming at proving automatically the absence of run time errors...
  • Tyrolean

  • Referenced in 89 articles [sw07830]
  • TTT2) is a tool for automatically proving (and disproving) termination of term rewrite systems...
  • HOL

  • Referenced in 591 articles [sw05492]
  • proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish...
  • MetiTarski

  • Referenced in 52 articles [sw00573]
  • proved automatically by MetiTarski: a resolution theorem prover (Metis) modified to call a decision procedure...
  • SPARK

  • Referenced in 48 articles [sw03124]
  • process of proving freedom from run-time errors can be performed automatically. The study identifies ... effective as possible in automatically proving absence of run-time errors.par The results will...
  • MU-TERM

  • Referenced in 34 articles [sw10015]
  • term: A Tool for Proving Termination of Context-Sensitive Rewriting. Restrictions of rewriting can eventually ... tool which can be used to automatically prove termination of CSR. The tool implements...
  • CLAM

  • Referenced in 41 articles [sw19619]
  • interactive proof editor into a fully automatic theorem proving system...
  • ETPS

  • Referenced in 160 articles [sw06302]
  • used to prove theorems of first- and higher-order logic interactively, automatically...
  • CeTA

  • Referenced in 47 articles [sw06584]
  • using CeTA. There are many automatic tools to prove termination of term rewrite systems, nowadays ... theorem prover Isabelle/HOL to automatically certify termination proofs. To this end, we first formalized...
  • SLAyer

  • Referenced in 21 articles [sw09712]
  • program analysis tool designed to automatically prove memory safety of industrial systems code. In this...
  • Epsilon

  • Referenced in 44 articles [sw00244]
  • inequations, and handle and prove geometric theorems automatically...
  • ML

  • Referenced in 522 articles [sw01218]
  • polymorphic Hindley–Milner type system, which automatically assigns the types of most expressions without requiring ... such as in compiler writing, automated theorem proving and formal verification. (wikipedia...
  • Walnut

  • Referenced in 30 articles [sw30122]
  • Automatic Theorem Proving in Walnut. Walnut is a software package that implements a mechanical decision ... some special words referred to as automatic words or automatic sequences. Walnut is written...
  • IsaPlanner

  • Referenced in 30 articles [sw02047]
  • used to conjecture and prove theorems automatically. The system provides an interactive tracing tool that...
  • TORPA

  • Referenced in 10 articles [sw10120]
  • TORPA: Termination of rewriting proved automatically. The tool TORPA (Termination of Rewriting Proved Automatically ... used to prove termination of string rewriting systems (SRSs) fully automatically. The underlying techniques include...
  • CVC4

  • Referenced in 124 articles [sw09485]
  • automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove...
  • TPA

  • Referenced in 13 articles [sw10114]
  • Termination Proved Automatically. TPA is a tool for proving termination of term rewrite systems (TRSs...
  • HipSpec

  • Referenced in 14 articles [sw07736]
  • HipSpec is a system for automatically deriving and proving properties about functional programs. It uses ... exploration, counterexample testing and inductive theorem proving. HipSpec automatically generates a set of equational theorems ... used as a background theory for proving additional user-stated properties. Experimental results are encouraging...
  • Nominal Isabelle

  • Referenced in 76 articles [sw12055]
  • Isabelle/HOL theorem prover. It provides a proving infrastructure for reasoning about programming language calculi involving ... establishes automatically the reasoning infrastructure for α-equated terms. We also prove strong induction principles...
  • TPS

  • Referenced in 73 articles [sw00973]
  • used to prove theorems of first- and higher-order logic interactively, automatically...