• Isabelle/HOL

  • Referenced in 578 articles [sw01569]
  • mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...
  • SPIN

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

  • Referenced in 537 articles [sw04702]
  • integrated tool environment for modeling, simulation and verification of real-time systems, developed jointly...
  • PVS

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

  • Referenced in 440 articles [sw16554]
  • single object, and finally performing verification through least-squares solution for consistent pose parameters. This...
  • Isabelle

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

  • Referenced in 231 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 268 articles [sw04125]
  • verified by symbolic model checking. If the verification fails, then HyTech generates a diagnostic error...
  • z3

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

  • Referenced in 183 articles [sw06580]
  • formalization of mathematics and industrial formal verification...
  • BLAST

  • Referenced in 95 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 112 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...
  • UNITY

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

  • Referenced in 76 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...
  • CafeOBJ

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

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

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

  • Referenced in 121 articles [sw20012]
  • provide support for explicit or BDD-based verification tools that perform either bisimulation reduction...
  • MOCHA

  • Referenced in 75 articles [sw12935]
  • interactive software environment for system specification and verification. The main objective of MOCHA ... rather than destroy, design structure in automatic verification. MOCHA is intended as a vehicle ... development of new verification algorithms and approaches. MOCHA is available in two versions, cMocha (Version...
  • OBJ3

  • Referenced in 98 articles [sw05370]
  • theorem proving, user interface design, and hardware verification, among other things. It was the first...