• Why3

  • Referenced in 136 articles [sw04438]
  • Why3 is a platform for deductive program verification. It provides a rich language for specification...
  • WhyML

  • Referenced in 28 articles [sw09709]
  • present Why3, a tool for deductive program verification, and WhyML, its programming and specification language...
  • F*

  • Referenced in 20 articles [sw27563]
  • program verification. It puts together the automation of an SMT-backed deductive verification tool with ... assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml...
  • STeP

  • Referenced in 36 articles [sw17948]
  • combines model checking with deductive methods to allow the verification of a broad class ... component) circuit designs, parameterized (N-process) programs, and programs with infinite data domains...
  • KeY-C

  • Referenced in 5 articles [sw00486]
  • tool for deductive verification of C programs. KeY-C allows to prove partial correctness...
  • ETPS

  • Referenced in 161 articles [sw06302]
  • automated theorem proving include hardware and software verification, partial automation of various mathematical activities, promoting ... theories in a wide variety of disciplines, deductive information systems for these disciplines, expert systems ... these into natural deduction proofs, constructing natural deduction proofs, translating natural deduction proofs which ... interactive facilities of TPS for constructing natural deduction proofs have been used under the name...
  • KeYmaera

  • Referenced in 48 articles [sw03709]
  • verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies ... theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential ... valued first-order dynamic logic for hybrid programs, a program notation for hybrid automata...
  • Jessie

  • Referenced in 3 articles [sw22719]
  • Jessie plug-in allows deductive verification of C programs annotated with ACSL. It uses internally...
  • Mcmt

  • Referenced in 24 articles [sw11911]
  • describe mcmt, a fully declarative and deductive symbolic model checker for safety properties of infinite ... been successfully applied to the verification of imperative programs, parametrised, timed, and distributed systems...
  • JKelloy

  • Referenced in 2 articles [sw09964]
  • Several tools support Alloy specifications for Java programs. However, they can only check the validity ... presents JKelloy, a tool for deductive verification of Java programs with Alloy specifications. It includes...
  • RGITL

  • Referenced in 6 articles [sw13917]
  • extends ITL with explicit interleaved programs and recursive procedures. Deduction is based on the principles ... symbolic execution and induction, known from the verification of sequential programs, which are transferred...
  • CoVaC

  • Referenced in 7 articles [sw21472]
  • deductive framework for proving program equivalence and its application to automatic verification of transformations performed...
  • KeY-ABS

  • Referenced in 3 articles [sw39518]
  • tool for deductive verification of concurrent and distributed programs written in ABS. KeY-ABS allows...
  • Ivy

  • Referenced in 10 articles [sw41668]
  • verification using an SMT solver, abstraction and model checking, and manual proofs using natural deduction ... model checking. Ivy can extract executable distributed programs by translation to efficient C++ code ... counterexamples, automatically audits proofs for decidability of verification conditions, and provides modular hiding of theories...
  • VeriCon

  • Referenced in 5 articles [sw16297]
  • either confirms the correctness of the controller program on all admissible network topologies or outputs ... then implements classical Floyd-Hoare-Dijkstra deductive verification using Z3. Our preliminary experience indicates that ... large repertoire of simple core SDN programs. VeriCon is compositional, in the sense that...
  • BVD

  • Referenced in 3 articles [sw13938]
  • potential program errors reported by a deductive program verifier. The user interface is like that ... statically without executing the program. BVD integrates with the program-verification engine Boogie. Just...
  • Guardol

  • Referenced in 2 articles [sw28543]
  • verification support. Guard programs and specifications are translated to higher order logic, then deductively transformed...
  • Cuneiform

  • Referenced in 1 article [sw26049]
  • context of functional programming. Moreover, the simple type system allows the deduction of the language ... formulation of the semantics also permits the verification of compilers to and from other workflow...
  • KERNELC

  • Referenced in 1 article [sw38622]
  • Abstract contract synthesis and verification in the symbolic K framework. In this article, we propose ... used for automatically inferring software contracts from programs that are written in a non-trivial ... using other (observer) routines in the same program. We implemented our technique in the automated ... integrated support for symbolic execution and deductive verification provided by 𝕂, some synthesized axioms that...
  • SHIP

  • Referenced in 1 article [sw14071]
  • programming language representing states in Description Logics and state transitions as logical updates enabling deductive ... runtime verification by splitting a process into a subprocess executing some critical program and another...