• SPIN

  • Referenced in 721 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 128 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...
  • Isabelle/HOL

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

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

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

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

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

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

  • Referenced in 38 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...
  • SatAbs

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

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

  • Referenced in 154 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 91 articles [sw12935]
  • growing interactive software environment for system specification and verification. The main objective of MOCHA...
  • VERSOFT

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

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

  • Referenced in 16 articles [sw18274]
  • this paper, we present SeaHorn, a software verification framework. The key distinguishing feature of SeaHorn ... procedural technique, (b) provides flexibility in the verification semantics to allow different levels of precision ... software model checking and abstract interpretation for verification, and (d) uses Horn-clauses ... customizable framework for experimenting with new software verification techniques. The effectiveness and scalability of SeaHorn...
  • UFO

  • Referenced in 22 articles [sw09570]
  • Framework for Abstraction- and Interpolation-Based Software Verification. In this paper, we present...
  • OBJ3

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

  • Referenced in 18 articles [sw07396]
  • Predator is a tool for automated formal verification of sequential C programs operating with pointers ... describes its participation in the Software Verification Competition SV-COMP’13 held at TACAS...
  • Gappa

  • Referenced in 18 articles [sw04885]
  • backend prover for the Why software verification plateform or as an automatic tactic...