• SPIN

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

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

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

  • Referenced in 229 articles [sw04131]
  • verification tools, as a testbed for formal verification techniques, and applied to other research areas...
  • UNITY

  • Referenced in 149 articles [sw13461]
  • formal assertions, permitting formal verification of the transition systems, and second into an executable program ... transition systems: one can specify properties formally that the model should obey and prove them...
  • HOL Light

  • Referenced in 138 articles [sw06580]
  • formalization of mathematics and industrial formal verification...
  • KeY

  • Referenced in 47 articles [sw09969]
  • integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly...
  • Isabelle/ZF

  • Referenced in 44 articles [sw04973]
  • mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware ... properties of computer languages and protocols. Isabelle/ZF formalizes the greater part of elementary set theory...
  • seL4

  • Referenced in 27 articles [sw15222]
  • seL4: formal verification of an OS kernel. Complete formal verification is the only known ... experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract ... used a unique design approach that fuses formal and operating systems techniques. To our knowledge...
  • MathSAT

  • Referenced in 40 articles [sw09449]
  • explicitly designed for being used in formal verification, and thus provides functionalities which extend...
  • PVS

  • Referenced in 471 articles [sw03484]
  • verification system: that is, a specification language integrated with support tools and a theorem prover ... state-of-the-art in mechanized formal methods and to be sufficiently rugged that...
  • STeP

  • Referenced in 26 articles [sw17948]
  • group to support the computer-aided formal verification of reactive, real-time and hybrid systems...
  • CompCert

  • Referenced in 23 articles [sw09737]
  • CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such ... guarantees that can be obtained by applying formal methods to source programs. The main result...
  • Cadence SMV

  • Referenced in 23 articles [sw07795]
  • possible input sequences. While formal verification is often equated with equivalence checking, model checking...
  • ETPS

  • Referenced in 127 articles [sw06302]
  • software verification, partial automation of various mathematical activities, promoting development of formal theories...
  • FoCs

  • Referenced in 16 articles [sw01591]
  • FoCs -- automatic generation of simulation checkers from formal specifications. For the foreseeable future, industrial hardware ... simulation and model checking in the design verification process. To date, these techniques are applied ... individual advantages of simulation and formal verification...
  • Checkfence

  • Referenced in 15 articles [sw09939]
  • CheckFence is a SAT-based formal verification tool that analyzes C code implementing concurrent data ... interleavings and reorderings. CheckFence does not require formal specifications or annotations, but mines a specification...
  • ABC

  • Referenced in 10 articles [sw12910]
  • domain system for logic synthesis and formal verification of binary logic circuits appearing in synchronous ... synergy of sequential synthesis and sequential verification leads to improvements in both domains. This paper ... development, and illustrates its use in formal verification...
  • CVT

  • Referenced in 14 articles [sw09952]
  • code validation tool (CVT). Automatic verification of a compilation process. We describe CVT -- a fully ... viable alternative to a full formal verification of the code-generator program...
  • WoLFram

  • Referenced in 13 articles [sw02075]
  • WoLFram -- a word level framework for formal verification and its application. A framework that automatically ... WoLFram is successfully applied to the verification of PLC programs. Equivalence checking and property checking ... shown, that modern SAT solvers can formally verify PLC programs within a short run time...