Why3
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Apron
- ACL2
- Cocktail
- Coq
- CPBPV
- Dafny
- HOL-Boogie
- KeY-C
- Shellcheck
- CoLiS
- Whiley
- solgraph
- EthVer
- ARQMath
- JDD
- BDD
- Sylvan
- RelView
- Alloy
- COMBINE
- IMP++
- RealLib
- TVOC
- SPARK
- KRAKATOA
- Eiffel
- A set solver for finite set relation algebra
- Tests and proofs for custom data generators
- A formally verified interpreter for a shell-like programming language
- A semi-automatic proof of strong connectivity
- Verifying branch-free assembly code in Why3
- How to get an efficient yet verified arbitrary-precision integer library
- Automating the verification of floating-point programs
- ACSL
- Instrumenting a weakest precondition calculus for counterexample generation
- Daikon
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- Hammer for Coq: automation for dependent type theory
- JML
- Spec#
- Omnibus
- distcc
- Caduceus
- Frama-C
- Deciding local theory extensions via E-matching
- Selected extended papers of VSTTE 2016
- Automated verification of functional correctness of race-free GPU programs
- The matrix reproved (verification pearl)
- Gappa
- cvc3
- z3
- Alt-Ergo
- TASS_
- ISP
- core 2
- SIMPLIFY
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Netsoft
- A Coq formalisation of SQL's execution engines
- Understanding parameters of deductive verification: an empirical investigation of KeY
- A Why3 framework for reflection proofs and its application to GMP's algorithms
- A FOOLish encoding of the next state relations of imperative programs
- FocalTest
- Flocq
- MUNCH
- ESC/Java
- ESC4
- VCC
- SANTE
- ATGen
- Programming languages and systems. 22nd European symposium on programming, ESOP 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16--24, 2013. Proceedings
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- TASS: the toolkit for accurate scientific software
- FEVS: a functional equivalence verification suite for high-performance scientific computing
- A system for compositional verification of asynchronous objects
- Chalice
- VeriFast
- Boogie
- An assertional proof of red-black trees using Dafny
- JACK
- Simpler proofs with decentralized invariants
- Superposition with first-class booleans and inprocessing clausification
- PolyPaver
- Verifying Whiley programs with Boogie
- Leon
- Coq/SSReflect
- MARMOT
- Automated verification of the parallel Bellman-Ford algorithm
- TRACER
- CVC4
- Verifying the conversion into CNF in dafny
- WhyML
- SLAyer
- K tool
- VeriCool
- Computer-assisted verification of four interval arithmetic operators
- Smallfoot
- SLAB
- KeY
- PAF!
This page was built for software: Why3
