• Why3

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

  • Referenced in 25 articles [sw04657]
  • level bounded model checking, correspondence checking, deductive verification, and predicate abstraction-based verification...
  • F*

  • Referenced in 19 articles [sw27563]
  • automation of an SMT-backed deductive verification tool with the expressive power of a proof...
  • WhyML

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

  • Referenced in 153 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...
  • STeP

  • Referenced in 36 articles [sw17948]
  • combines model checking with deductive methods to allow the verification of a broad class...
  • KeYmaera

  • Referenced in 40 articles [sw03709]
  • hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover ... theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential...
  • TPS

  • Referenced in 71 articles [sw00973]
  • 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...
  • InVeSt

  • Referenced in 10 articles [sw12034]
  • state systems. In VeSt integrates deductive and algorithmic verification principles for the verification of invariance...
  • KeY-C

  • Referenced in 5 articles [sw00486]
  • present KeY-C, a tool for deductive verification of C programs. KeY-C allows...
  • SAD

  • Referenced in 14 articles [sw09796]
  • System for automated deduction (SAD): A tool for proof verification. In this paper a proof...
  • Jessie

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

  • Referenced in 3 articles [sw16297]
  • then implements classical Floyd-Hoare-Dijkstra deductive verification using Z3. Our preliminary experience indicates that...
  • InvA

  • Referenced in 2 articles [sw10124]
  • tool. The InvA tool supports the deductive verification of safety properties of infinite-state concurrent...
  • JKelloy

  • Referenced in 2 articles [sw09964]
  • paper presents JKelloy, a tool for deductive verification of Java programs with Alloy specifications...
  • TLPVS

  • Referenced in 10 articles [sw10024]
  • implementation of a linear temporal logic verification system. The system includes a set of theories ... deductive ltl system. A distributed rank rule for the verification of response properties in parameterized...
  • CoVaC

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

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

  • Referenced in 5 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...