swMATH183MaRDI QIDQ12950FDOQ12950
Author name not available (Why is that?)
Official website: http://research.microsoft.com/en-us/projects/dafny/
Cited In (only showing first 100 items - show all)
- Efficient verification of imperative programs using auto2
- Boolector
- ACSL
- Caduceus
- JML
- Frama-C
- Why3
- Spec#
- SIMPLIFY
- z3
- KRoC
- Rodin
- ESC/Java
- ESC4
- CPAchecker
- MathBrush
- VCC
- Ultimate Automizer
- Boogie
- Chalice
- HipSpec
- VeriFast
- Zeno
- OpenSMT
- versat
- Leon
- TRX
- CVC4
- cminor
- evt
- HIP
- Smallfoot
- KeY
- Toolchain
- TLAPS
- TLC
- Qex
- KIV
- WhyML
- Ivy
- VeriCool
- VeriSmall
- TVLA
- Viper
- Hipster
- GPUVerify
- jStar
- VerCors
- FDR3
- TTM
- ModuRes
- SymDiff
- CSSV
- YOGI
- TweetNaCl
- Lingva
- Grasshopper
- VERL
- BVD
- Clara
- GNATprove
- RGITL
- DynaMate
- EventB2Dafny
- VeriCon
- PSync
- ARMor
- AUSPICE-R
- coreStar
- SeaHorn
- Graphsc
- CacBDD
- c2i
- Pirate
- CafeInMaude
- OpenJML
- Caper
- C-Light
- RADA
- CertiKOS
- MarQ
- MoCHi
- StaRVOOrS
- VACID-0
- Charge!
- Verdi
- Jessie
- VeriFun
- GRASShopper
- H-PILoT
- SMACK
- AstraVer
- F*
- LiquidHaskell
- Rust
- VST-Floyd
- VST-Floyd: a separation logic tool to verify correctness of C programs
- Verification of concurrent systems with VerCors
- AUSPICE-R: automatic safety-property proofs for realistic features in machine code
- Loop summarization using state and transition invariants
This page was built for software: Dafny
