• SPIN

  • Referenced in 651 articles [sw03455]
  • Spin is a popular open-source software tool, used by thousands of people worldwide, that ... used for the formal verification of distributed software systems. The tool was developed at Bell...
  • BLAST

  • Referenced in 97 articles [sw02937]
  • BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool ... such verification in the Linux Driver Verification project. You may download source code or binary ... components it relies on are free software. The BLAST itself is released under Apache...
  • ETPS

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

  • Referenced in 399 articles [sw00454]
  • particular formal verification, which includes proving the correctness of computer hardware or software and proving...
  • Isabelle/HOL

  • Referenced in 396 articles [sw01569]
  • particular formal verification, which includes proving the correctness of computer hardware or software and proving...
  • TPS

  • Referenced in 64 articles [sw00973]
  • automated theorem proving include hardware and software verification, partial automation of various mathematical activities, promoting...
  • MAGIC

  • Referenced in 35 articles [sw14159]
  • simulation conformance. MAGIC is a software verification project for C source code which verifies conformance ... specifications. To this aim, MAGIC extracts abstract software models using predicate ahstraction, and resolves ... core principles implemented in the MAGIC verification engine, i.e., specification conformance using simulation and abstraction...
  • PolyBoRi

  • Referenced in 33 articles [sw00723]
  • growing importance of formal hardware and software verification based on Boolean expressions, which suffer-besides...
  • SatAbs

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

  • Referenced in 26 articles [sw07408]
  • open-source framework for software verification, based on the concepts of configurable program analysis...
  • SLAM

  • Referenced in 140 articles [sw03136]
  • software engineers in designing interfaces and software that ensure reliable and correct functioning. Static Driver ... Driver Development Kit that uses the SLAM verification engine...
  • MOCHA

  • Referenced in 77 articles [sw12935]
  • growing interactive software environment for system specification and verification. The main objective of MOCHA...
  • KeY

  • Referenced in 51 articles [sw09969]
  • implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible...
  • PPL

  • Referenced in 52 articles [sw05357]
  • systems for the analysis and verification of hardware and software components. Current applications span imperative...
  • OBJ3

  • Referenced in 121 articles [sw05370]
  • software design and specification, rapid prototyping, theorem proving, user interface design, and hardware verification, among...
  • VERSOFT

  • Referenced in 13 articles [sw10881]
  • VERSOFT: Verification software in MATLAB/INTLAB: VERSOFT is a collection of verification files for computing verified...
  • UCLID

  • Referenced in 21 articles [sw04657]
  • correctness of models of hardware and software systems. UCLID can be used to model ... level bounded model checking, correspondence checking, deductive verification, and predicate abstraction-based verification ... explored to-date include microprocessor design verification, analyzing software for security exploits, and verifying distributed...
  • Bogor

  • Referenced in 45 articles [sw06858]
  • Building your own software model checker using the Bogor extensible model checking framework Model checking ... technology for verification and debugging in hardware and more recently in software domains. We believe...
  • Cogent

  • Referenced in 9 articles [sw01300]
  • proving for program verification Many symbolic software verification engines such as Slam and ESC/Java rely...
  • CSIsat

  • Referenced in 10 articles [sw11407]
  • tool on benchmarks from software verification. Binaries and the source code of CSIsat are publicly...