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