Cited in
(only showing first 100 items - show all)- Static contract checking with abstract interpretation
- Efficient verification of imperative programs using auto2
- Contract-based verification of MATLAB-style matrix programs
- WhyMP, a formally verified arbitrary-precision integer library
- WhyMP, a formally verified arbitrary-precision integer library
- Secure distributed programming with value-dependent types
- Deciding local theory extensions via E-matching
- Viper
- Drools
- MLton
- THOR
- GMac
- Haskabelle
- Grail
- coreStar
- Atoment
- CoqMT
- Java Jr
- Graphsc
- CacBDD
- Pirate
- DifferenceDifferential
- OpenJML
- MiniMaple
- C-Light
- Fiat
- BoogiePL
- MathComp.tuple
- Luck
- Hume
- Ssreflect.fintype
- VACID-0
- foetus
- Verdi
- Jessie
- VeriFun
- H-PILoT
- VeriMAP
- BIGNUM
- ASMKeY
- KLEE-FP
- JBMC
- HARP
- CIL
- AstraVer
- HoTTSQL
- F*
- LiquidHaskell
- Camelot
- Coq Interval
- Bedrock
- AVL trees
- RealCertify
- TiML
- Dijkstra Shortest Path
- Flow Networks
- Guardol
- Equations
- Graph Theory
- Refinement Monadic
- Separation Logic
- Q*cert
- SEQUEL
- Focalide
- SPL Conqueror
- SQLCert
- Treaps
- Maximum Cardinality Matching
- AutoProof
- RVT
- CoqInE
- ArchSAT
- Auto2_Imperative_HOL
- Logipedia
- PQL
- Regular_Algebras
- ShortestPath
- Simpl
- Zipperposition
- STLlint
- SMT proof checking using a logical framework
- Manticore
- Silq
- HACL*
- WhyMP
- Metamath Zero
- FreeSpec
- Binutils
- Mythril
- Probabilistic_Prime_Tests
- Prpu_Maxflow
- Daisy
- Wombit
- Nagini
- QF_FP
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Hammer for Coq: automation for dependent type theory
- Wombit: a portfolio bit-vector solver using word-level propagation
- CPBPV: a constraint-programming framework for bounded program verification
This page was built for software: Why3
