• SPIN

  • Referenced in 555 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 95 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 127 articles [sw06302]
  • automated theorem proving include hardware and software verification, partial automation of various mathematical activities, promoting...
  • Isabelle

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

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

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

  • Referenced in 32 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 34 articles [sw00723]
  • growing importance of formal hardware and software verification based on Boolean expressions, which suffer-besides...
  • CPAchecker

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

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

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

  • Referenced in 121 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...
  • PPL

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

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

  • Referenced in 14 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...
  • OBJ3

  • Referenced in 96 articles [sw05370]
  • software design and specification, rapid prototyping, theorem proving, user interface design, and hardware verification, among...
  • Lambda-Clam

  • Referenced in 19 articles [sw19614]
  • outlined, in particular the synthesis and verification of software and hardware systems...
  • 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...