Results 21 to 40 of 269
Sort by:

  • 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...