Cited in
(only showing first 100 items - show all)- Ensuring correctness of model transformations while remaining decidable
- Loop summarization using state and transition invariants
- An assertional proof of the stability and correctness of Natural Mergesort
- A learning-based approach to synthesizing invariants for incomplete verification engines
- An assertional proof of red-black trees using Dafny
- Theory and techniques for synthesizing efficient breadth-first search algorithms
- Heaps and Data Structures: A Challenge for Automated Provers
- Automata-theoretic semantics of idealized Algol with passive expressions
- Verifying Whiley programs with Boogie
- Formal verification of a Java component using the RESOLVE framework
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
- Product programs in the wild: retrofitting program verifiers to check information flow security
- Indexed and fibred structures for Hoare logic
- Efficient verification of imperative programs using auto2
- Modular synthesis of sketches using models
- CRADLE
- Modular verification of procedure equivalence in the presence of memory allocation
- Verifying visibility-based weak consistency
- Synchronizing the asynchronous
- Taking satisfiability to the next level with Z3 (abstract)
- Contract-based verification of MATLAB-style matrix programs
- Alloy*: a general-purpose higher-order relational constraint solver
- Automating theorem proving with SMT
- Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018
- The relationship between separation logic and implicit dynamic frames
- Collaborative verification and testing with explicit assumptions
- Fifty years of Hoare's logic
- Viper: a verification infrastructure for permission-based reasoning
- TIP: tons of inductive problems
- Bounded quantifier instantiation for checking inductive invariants
- Local reasoning for global graph properties
- Simpler proofs with decentralized invariants
- Automated verification of parallel nested DFS
- Two-level mixed verification method of C-light programs in terms of safety logic
- Building program construction and verification tools from algebraic principles
- Quicksort revisited. Verifying alternative versions of quicksort
- Automating deductive verification for weak-memory programs
- Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
- MoSeL
- Indexed and fibered structures for partial and total correctness assertions
- Enforcing structural invariants using dynamic frames
- Automated verification of the parallel Bellman-Ford algorithm
- Verifying the conversion into CNF in dafny
- Boolector
- KeY-C
- ArcAngel
- KRAKATOA
- Eiffel
- 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
This page was built for software: Dafny
