• ML

  • Referenced in 517 articles [sw01218]
  • compiler writing, automated theorem proving and formal verification. (wikipedia...
  • PVS

  • Referenced in 620 articles [sw03484]
  • verification system: that is, a specification language integrated with support tools and a theorem prover...
  • ETPS

  • Referenced in 156 articles [sw06302]
  • Potential applications of automated theorem proving include hardware and software verification, partial automation of various ... intelligence. TPS can be used to prove theorems of first- and higher-order logic interactively...
  • z3

  • Referenced in 509 articles [sw04887]
  • high-performance theorem prover being developed at Microsoft Research.Z3 supports linear real and integer arithmetic ... number of program analysis, testing, and verification tools from Microsoft Research. These include: VCC, Spec...
  • Why3

  • Referenced in 130 articles [sw04438]
  • Why3 is a platform for deductive program verification. It provides a rich language for specification ... relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes...
  • OBJ3

  • Referenced in 138 articles [sw05370]
  • specification, rapid prototyping, theorem proving, user interface design, and hardware verification, among other things...
  • Z/EVES

  • Referenced in 43 articles [sw10262]
  • specifications in CZT with theorem proving and verification capabilities. Z/EVES Eclipse provides a modern environment...
  • TPS

  • Referenced in 71 articles [sw00973]
  • Potential applications of automated theorem proving include hardware and software verification, partial automation of various ... intelligence. TPS can be used to prove theorems of first- and higher-order logic interactively...
  • KeYmaera

  • Referenced in 41 articles [sw03709]
  • hybrid theorem prover for hybrid systems. KeYmaera is a hybrid verification tool for hybrid systems ... automated and interactive theorem prover for a natural specification and verification logic for hybrid systems...
  • HOL Light

  • Referenced in 293 articles [sw06580]
  • Mike Gordon’s original HOL system. Theorem provers in this family use a version ... formalization of mathematics and industrial formal verification...
  • WhyML

  • Referenced in 25 articles [sw09709]
  • mutable fields, type invariants, and ghost code. Verification conditions are discharged by Why3 with ... various existing automated and interactive theorem provers. To keep verification conditions tractable and comprehensible, WhyML...
  • jStar

  • Referenced in 32 articles [sw11261]
  • automatic verification system, called jStar, which combines theorem proving and abstract interpretation techniques. We demonstrate ... been highly challenging for existing object-oriented verification techniques...
  • UNITY

  • Referenced in 184 articles [sw13461]
  • formal assertions, permitting formal verification of the transition systems, and second into an executable program ... model should obey and prove them as theorems using the formal specification. The methodology...
  • LOOP

  • Referenced in 29 articles [sw10292]
  • front-end to a theorem prover in which the actual verification of the desired properties...
  • Cogent

  • Referenced in 14 articles [sw01300]
  • Cogent: Accurate theorem proving for program verification. Many symbolic software verification engines such as Slam...
  • KeY

  • Referenced in 63 articles [sw09969]
  • integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly ... core of the system is a novel theorem prover for the first-order Dynamic Logic...
  • CakeML

  • Referenced in 46 articles [sw08799]
  • machine code. Our correctness theorem ensures that this REPL implementation prints only those results permitted ... semantics of CakeML. Our verification effort touches on a breadth of topics including lexing, parsing ... more challenging aspects of the verification. In particular, our formally verified compiler can bootstrap itself ... development was carried out in the HOL4 theorem prover...
  • Alt-Ergo

  • Referenced in 16 articles [sw04888]
  • Ergo is an automatic theorem prover dedicated to program verification. Alt-Ergo is based...
  • TVOC

  • Referenced in 19 articles [sw02521]
  • proof rule Validate. Verification conditions are validated using the automatic theorem prover CVC Lite...
  • evt

  • Referenced in 7 articles [sw09805]
  • main outcome is the ERLANG Verification Tool (EVT), a theorem prover which assists in obtaining ... recursion. We give a summary of the verification framework as supported by EVT, discuss reasoning ... summarised, and an approach for supporting verification in the presence of program libraries is outlined ... essentially a classical proof assistant, or theorem-proving tool, requiring users to intervene...