• 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 real-time systems...
  • Esterel

  • Referenced in 166 articles [sw20012]
  • support for explicit or BDD-based 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 free-variable ... 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 Industrial-Strength Verification Tool. ABC is a public-domain system for logic synthesis...
  • CMC

  • Referenced in 34 articles [sw12422]
  • Systems. In this paper we present a tool (CMC) for compositional model-checking of real ... method compared to existing real-time 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 special-purpose verification tool, written in Prolog, that has been developed...