
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 abstractionbased verification...

F*
 Referenced in 19 articles
[sw27563]
 automation of an SMTbacked 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...

KeYC
 Referenced in 5 articles
[sw00486]
 present KeYC, a tool for deductive verification of C programs. KeYC 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 plugin allows deductive verification of C programs annotated with ACSL. It uses internally...

VeriCon
 Referenced in 3 articles
[sw16297]
 then implements classical FloydHoareDijkstra 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 infinitestate 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...

MCMASX
 Referenced in 3 articles
[sw02864]
 Verification of the TESLA protocol in MCMASX. We use MCMASX to verify authentication ... explicit and deductive knowledge of the OBDDbased model checker MCMAS a verification tool...