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

NuSMV
 Referenced in 314 articles
[sw04131]
 designs, as a core for custom verification tools, as a testbed for formal verification techniques...

SPIN
 Referenced in 727 articles
[sw03455]
 used for the formal verification of distributed software systems. The tool was developed at Bell...

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

Uppaal
 Referenced in 658 articles
[sw04702]
 Uppaal is an integrated tool environment for modeling, simulation and verification of realtime systems...

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

Boogie
 Referenced in 120 articles
[sw07714]
 also the name of the verification tool that takes Boogie programs as input. Boogie ... also the name of a tool. The tool accepts the Boogie language as input, optionally ... given Boogie program, and then generates verification conditions that are passed to an SMT solver...

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

Isabelle/HOL
 Referenced in 1025 articles
[sw01569]
 expressed in a formal language and provides tools for proving those formulas in a logical ... mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...

Isabelle
 Referenced in 719 articles
[sw00454]
 expressed in a formal language and provides tools for proving those formulas in a logical ... mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...

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

Caduceus
 Referenced in 63 articles
[sw04625]
 Caduceus used to be a verification tool for C programs built...

KeYmaera
 Referenced in 48 articles
[sw03709]
 hybrid systems. KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real ... theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential ... notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized freevariable ... following an iterative background closure strategy. Our tool is particularly suitable for verifying parametric hybrid...

SatAbs
 Referenced in 41 articles
[sw12804]
 predicate abstraction refinement loop. Existing software verification tools such as Slam, Blast, or Magic...

JPAX
 Referenced in 30 articles
[sw09906]
 overview of the runtime verification tool Java PathExplorer. We present an overview of the Java ... PathExplorer runtime verification tool, in short referred to as JPAX. JPAX can monitor the execution ... analysis requires no user provided specification. The tool facilitates automated instrumentation of a program ... specialized analysis, such as the temporal logic verification, the deadlock analysis and the data race...

ABC
 Referenced in 39 articles
[sw12910]
 Academic IndustrialStrength Verification Tool. ABC is a publicdomain system for logic synthesis...

CMC
 Referenced in 34 articles
[sw12422]
 Systems. In this paper we present a tool (CMC) for compositional modelchecking of real ... method compared to existing realtime verification tools (HYTECH, KRONOS, UPPAAL). After a description...

HyTech
 Referenced in 333 articles
[sw04125]
 HyTech is an automatic tool for the analysis of embedded systems. HyTech computes the condition ... verified by symbolic model checking. If the verification fails, then HyTech generates a diagnostic error ... standard reference to the HyTech tool...

d/dt
 Referenced in 37 articles
[sw10314]
 with linear differential inclusions. The d/dt tool for verification of hybrid systems. We describe ... tool d/dt which provides automatic safety verification of hybrid systems with linear continuous dynamics with ... uncertain input. The verification procedure is based on a method for overapproximating reachable sets ... orthogonal polyhedra. The tool also allows to synthesize a controller which switches the system between...

NRL
 Referenced in 34 articles
[sw12158]
 analyzer is a prototype specialpurpose verification tool, written in Prolog, that has been developed...