• PVS

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

  • Referenced in 134 articles [sw04438]
  • provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library ... extraction mechanism. WhyML is also used as an intermediate language for the verification...
  • UNITY

  • Referenced in 185 articles [sw13461]
  • coupled state transition systems. Mechanical methods for mapping the transition systems first into ... formal assertions, permitting formal verification of the transition systems, and second into an executable program...
  • MAYA

  • Referenced in 26 articles [sw03423]
  • specification which always endangers the verification work already done. In this paper we describe ... structured manner, incorporates a uniform mechanism for verification in-the-large to exploit the structure...
  • NuSMV

  • Referenced in 309 articles [sw04131]
  • Reasoning Group at University of Genova The Mechanized Reasoning Group at University of Trento. NuSMV ... which can be reliably used for the verification of industrial designs, as a core...
  • WhyML

  • Referenced in 26 articles [sw09709]
  • automated and interactive theorem provers. To keep verification conditions tractable and comprehensible, WhyML imposes ... extraction mechanism. WhyML is also used as an intermediate language for the verification...
  • LIRA

  • Referenced in 8 articles [sw21270]
  • integers and the reals. The mechanization of many verification tasks relies on efficient implementations...
  • HOLCF

  • Referenced in 3 articles [sw25266]
  • state of the art in program verification: HOLCF ’11 can reason about many program definitions ... case study, we present a fully mechanized verification of a model of concurrency based...
  • LTSA-WS

  • Referenced in 14 articles [sw10585]
  • service implementations. The tool supports verification of properties created from design specifications and implementation models ... implementations are mechanically translated to FSP to allow an equivalence trace verification process...
  • ArchC

  • Referenced in 2 articles [sw07845]
  • features are a storage-based co-verification mechanism that automatically checks the consistency...
  • Constructive Proof FLP

  • Referenced in 2 articles [sw28832]
  • Mechanical verification of a constructive proof for FLP. The impossibility of distributed consensus with...
  • CakeML

  • Referenced in 52 articles [sw08799]
  • implementation of ML. We have developed and mechanically verified an ML system called CakeML, which ... permitted by the semantics of CakeML. Our verification effort touches on a breadth of topics...
  • PGWFT

  • Referenced in 3 articles [sw10573]
  • results show that our workflow verification and optimization mechanisms are feasible and efficient...
  • BWare

  • Referenced in 6 articles [sw10405]
  • aims to provide a mechanized framework to support the automated verification of proof obligations coming...
  • Jerboa

  • Referenced in 1 article [sw10051]
  • editor is equipped with many static verification mechanisms that ensure that the generated modelers only...
  • Alt-Ergo

  • Referenced in 16 articles [sw04888]
  • automatic theorem prover dedicated to program verification. Alt-Ergo is based ... home made SAT-solver and an instantiation mechanism...
  • ProMoVer

  • Referenced in 4 articles [sw06738]
  • previously developed tool set for compositional verification of control flow safety properties, and provides appropriate ... mechanism for proof reuse that detects and minimizes the verification tasks resulting from changes...
  • RGITL

  • Referenced in 5 articles [sw13917]
  • interactive verification environment KIV. It has been used to mechanize various proofs of concurrent algorithms...
  • Milawa

  • Referenced in 20 articles [sw09977]
  • small kernel and a powerful reflection mechanism. We have used the HOL4 theorem prover ... have combined these results with our previous verification of an x86 machine-code implementation...
  • SHIP

  • Referenced in 1 article [sw14071]
  • into subprocesses this provides a mechanism for runtime verification by splitting a process into...