
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 higherorder logic interactively...

z3
 Referenced in 509 articles
[sw04887]
 highperformance 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 higherorder 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 objectoriented 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]
 frontend 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 objectoriented software as seamlessly ... core of the system is a novel theorem prover for the firstorder 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...

AltErgo
 Referenced in 16 articles
[sw04888]
 Ergo is an automatic theorem prover dedicated to program verification. AltErgo 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 theoremproving tool, requiring users to intervene...