
Isabelle/HOL
 Referenced in 1018 articles
[sw01569]
 mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...

SPIN
 Referenced in 723 articles
[sw03455]
 that can be used for the formal verification of distributed software systems. The tool...

Isabelle
 Referenced in 710 articles
[sw00454]
 mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...

Uppaal
 Referenced in 654 articles
[sw04702]
 integrated tool environment for modeling, simulation and verification of realtime systems, developed jointly...

SIFT
 Referenced in 631 articles
[sw16554]
 single object, and finally performing verification through leastsquares solution for consistent pose parameters. This...

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

z3
 Referenced in 594 articles
[sw04887]
 number of program analysis, testing, and verification tools from Microsoft Research. These include: VCC, Spec...

ML
 Referenced in 522 articles
[sw01218]
 compiler writing, automated theorem proving and formal verification. (wikipedia...

NuSMV
 Referenced in 309 articles
[sw04131]
 which can be reliably used for the verification of industrial designs, as a core ... custom verification tools, as a testbed for formal verification techniques, and applied to other research...

HyTech
 Referenced in 331 articles
[sw04125]
 verified by symbolic model checking. If the verification fails, then HyTech generates a diagnostic error...

HOL Light
 Referenced in 308 articles
[sw06580]
 formalization of mathematics and industrial formal verification...

BLAST
 Referenced in 129 articles
[sw02937]
 BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool ... point (main function) by a valid execution. Verification of safety properties may be reduced ... reachability, and BLAST is used for such verification in the Linux Driver Verification project...

CESAR
 Referenced in 161 articles
[sw08510]
 Specification and verification of concurrent systems in CESAR. The aim of this paper ... fixed points of monotonic predicate transformers. The verification of a system consists in obtaining...

Why3
 Referenced in 134 articles
[sw04438]
 Why3 is a platform for deductive program verification. It provides a rich language for specification ... provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library ... used as an intermediate language for the verification of C, Java, or Ada programs. Why3...

Boogie
 Referenced in 120 articles
[sw07714]
 Boogie: An Intermediate Verification Language. Boogie is an intermediate verification language, intended as a layer ... which is also the name of the verification tool that takes Boogie programs as input ... given Boogie program, and then generates verification conditions that are passed to an SMT solver...

UNITY
 Referenced in 185 articles
[sw13461]
 formal assertions, permitting formal verification of the transition systems, and second into an executable program...

CafeOBJ
 Referenced in 171 articles
[sw06232]
 CafeOBJ as a tool for behavioral system verification. We report on a machine supported method...

Esterel
 Referenced in 166 articles
[sw20012]
 provide support for explicit or BDDbased verification tools that perform either bisimulation reduction...

ETPS
 Referenced in 160 articles
[sw06302]
 automated theorem proving include hardware and software verification, partial automation of various mathematical activities, promoting...

SLAM
 Referenced in 153 articles
[sw03136]
 Driver Development Kit that uses the SLAM verification engine...