• Why3

• Referenced in 134 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 20 articles [sw27563]
• automation of an SMT-backed deductive verification tool with the expressive power of a proof...

• WhyML

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

• ETPS

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

• Ivy

• Referenced in 9 articles [sw41668]
• Distributed Algorithms. vy is a multi-modal verification tool for correct design and implementation ... infinite-state systems via three modes: deductive verification using an SMT solver, abstraction and model ... checking, and manual proofs using natural deduction. It supports light-weight formal methods via compositional ... counterexamples, automatically audits proofs for decidability of verification conditions, and provides modular hiding of theories...

• TPS

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

• VeriCon

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

• KeY-ABS

• Referenced in 3 articles [sw39518]
• deductive verification tool for the concurrent modelling language ABS. We present KeY-ABS, a tool ... deductive verification of concurrent and distributed programs written in ABS. KeY-ABS allows to verify...

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

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

• KERNELC

• Referenced in 1 article [sw38622]
• Abstract contract synthesis and verification in the symbolic K framework. In this article, we propose ... integrated support for symbolic execution and deductive verification provided by 𝕂, some synthesized axioms that...

• Mcmt

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