• 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...