Dafny
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Boolector
- KeY-C
- ROSMonitoring
- Marathon 2
- Synchrobench
- JDD
- BDD
- BtorMC
- ArcAngel
- KRAKATOA
- Eiffel
- ACSL
- Why3
- Toward compositional verification of interruptible OS kernels and device drivers
- VST-Floyd: a separation logic tool to verify correctness of C programs
- A formal proof generator from semi-formal proof documents
- JML
- Spec#
- Caduceus
- Frama-C
- Reasoning about algebraic data types with abstractions
- Deciding local theory extensions via E-matching
- z3
- The symbiosis of concurrency and verification: teaching and case studies
- SIMPLIFY
- KRoC
- Backwards and forwards with separation logic
- Relational parametricity and quotient preservation for modular (co)datatypes
- Towards verified handwritten calculational proofs (short paper)
- Unifying separation logic and region logic to allow interoperability
- A Why3 framework for reflection proofs and its application to GMP's algorithms
- Datatypes with shared selectors
- Rodin
- ESC/Java
- ESC4
- VCC
- Loop invariant synthesis in a combined abstract domain
- Stepwise refinement of heap-manipulating code in Chalice
- Ultimate Automizer
- CPAchecker
- MathBrush
- Chalice
- VeriFast
- Boogie
- Zeno
- HipSpec
- An assertional proof of red-black trees using Dafny
- Alloy*: a general-purpose higher-order relational constraint solver
- Quicksort revisited. Verifying alternative versions of quicksort
- versat
- Real-time solving of computationally hard problems using optimal algorithm portfolios
- OpenSMT
- Simpler proofs with decentralized invariants
- TRX
- Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Verifying Whiley programs with Boogie
- Leon
- Inductive benchmarks for automated reasoning
- Automated verification of the parallel Bellman-Ford algorithm
- CVC4
- Abstraction and subsumption in modular verification of C programs
- Verifying the conversion into CNF in dafny
- Toolchain
- TLAPS
- TLC
- Loop verification with invariants and contracts
- Generalized arrays for Stainless frames
- Traits: correctness-by-construction for free
- WhyML
- cminor
- VeriCool
- HIP
- Smallfoot
- VeriSmall
- evt
- TVLA
- Qex
- KeY
- KIV
- A learning-based approach to synthesizing invariants for incomplete verification engines
- Indexed and fibred structures for Hoare logic
- Ivy
- Loop summarization using state and transition invariants
- Fifty years of Hoare's logic
- Hipster
- VerCors
- GPUVerify
- jStar
- Efficient verification of imperative programs using auto2
- Automating deductive verification for weak-memory programs
- A verification-driven framework for iterative design of controllers
- TTM
- Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- FDR3
- SymDiff
- YOGI
- TweetNaCl
- ModuRes
- VERL
This page was built for software: Dafny
