• CoVaC

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

  • Referenced in 6 articles [sw13917]
  • Deduction is based on the principles of symbolic execution and induction, known from the verification...
  • MCMAS-X

  • Referenced in 3 articles [sw02864]
  • Verification of the TESLA protocol in MCMAS-X. We use MCMAS-X to verify authentication ... explicit and deductive knowledge of the OBDD-based model checker MCMAS a verification tool...
  • BVD

  • Referenced in 3 articles [sw13938]
  • Boogie verification debugger (tool paper). The Boogie Verification Debugger (BVD) is a tool that lets ... potential program errors reported by a deductive program verifier. The user interface is like that ... program. BVD integrates with the program-verification engine Boogie. Just as Boogie supports multiple language...
  • Guardol

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

  • Referenced in 8 articles [sw12933]
  • Synthia: Verification and synthesis for timed automata. Synthia is the first certifying model checker ... user. Such certificates are easy-to-validate deductive proofs that only reflect the specification-critical...
  • Cuneiform

  • Referenced in 1 article [sw26049]
  • Moreover, the simple type system allows the deduction of the language’s safety ... formulation of the semantics also permits the verification of compilers to and from other workflow...
  • Basic-REAL

  • Referenced in 1 article [sw21002]
  • level integrated approach to design, specification and verification of distributed system. The approach is based ... specifications of bREAL, (III) problem-oriented compositional deductive reasoning coupled with model-checking. The paper...
  • SHIP

  • Referenced in 1 article [sw14071]
  • state transitions as logical updates enabling deductive support to infer non-explicitly represented knowledge ... subprocesses this provides a mechanism for runtime verification by splitting a process into a subprocess...
  • Propositional Resolution

  • Referenced in 1 article [sw28841]
  • show that the unrestricted Resolution rule is deductive- complete, in the sense that ... with many applications in artificial intelligence and verification (for abductive reasoning, knowledge compilation, diagnosis, debugging...
  • Apron

  • Referenced in 69 articles [sw00045]
  • Apron: a library of numerical abstract domains for...
  • ACL2

  • Referenced in 283 articles [sw00060]
  • ACL2 is both a programming language in which...
  • CoCoA

  • Referenced in 654 articles [sw00143]
  • CoCoA is a system for Computations in Commutative...
  • Coq

  • Referenced in 1890 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Dafny

  • Referenced in 73 articles [sw00183]
  • Dafny is an imperative object-based language with...
  • GAP

  • Referenced in 3189 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • Isabelle

  • Referenced in 713 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • LEO-II

  • Referenced in 51 articles [sw00512]
  • LEO-II is a standalone, resolution-based higher...
  • Macaulay2

  • Referenced in 1923 articles [sw00537]
  • Macaulay2 is a software system devoted to supporting...