Dafny: an automatic program verifier for functional correctness
From MaRDI portal
Recommendations
Cited in
(97)- 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
- Quorum tree abstractions of consensus protocols
- RustHorn: CHC-based verification for Rust programs
- Heaps and Data Structures: A Challenge for Automated Provers
- Automata-theoretic semantics of idealized Algol with passive expressions
- Verifying Whiley programs with Boogie
- 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
- Flexible Correct-by-Construction Programming
- Succinct ordering and aggregation constraints in algebraic array theories
- Cogent: uniqueness types and certifying compilation
- Concise outlines for a complex logic: a proof outline checker for TaDA
- Modular verification of procedure equivalence in the presence of memory allocation
- Automating Induction with an SMT Solver
- Verifying visibility-based weak consistency
- Synchronizing the asynchronous
- Towards a dereversibilizer: fewer asserts, statically
- Contract-based verification of MATLAB-style matrix programs
- Alloy*: a general-purpose higher-order relational constraint solver
- The relationship between separation logic and implicit dynamic frames
- A solver for arrays with concatenation
- Lemmaless induction in trace logic
- Verification of mutable linear data structures and iterator-based algorithms in Dafny
- Bounded quantifier instantiation for checking inductive invariants
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Why3-do: the way of harmonious distributed system proofs
- Local reasoning for global graph properties
- Simpler proofs with decentralized invariants
- Automated verification of parallel nested DFS
- Building program construction and verification tools from algebraic principles
- A modeling concept for formal verification of OS-based compositional software
- Reachability modulo theories
- Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
- \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic
- Indexed and fibered structures for partial and total correctness assertions
- Enforcing structural invariants using dynamic frames
- Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
- Efficient modular SMT-based model checking of pointer programs
- Integrating ADTs in KeY and their application to history-based reasoning about collection
- Trace-based verification of imperative programs with I/O
- Dafny
- Trace Abstraction-Based Verification for Uninterpreted Programs
- Generalized arrays for Stainless frames
- Loop verification with invariants and contracts
- Regular model checking revisited
- Toward compositional verification of interruptible OS kernels and device drivers
- ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
- Real-time solving of computationally hard problems using optimal algorithm portfolios
- Certified abstract cost analysis
- Integrating ADTs in KeY and Their Application to History-Based Reasoning
- On algebraic array theories
- LCTD: test-guided proofs for C programs on LLVM
- Inductive benchmarks for automated reasoning
- Traits: correctness-by-construction for free
- An automatically verified prototype of the Android permissions system
- Unifying separation logic and region logic to allow interoperability
- Decision procedures for region logic
- Verifying and synthesizing software with recursive functions (invited contribution)
- An algebraic glimpse at bunched implications and separation logic
- scientific article; zbMATH DE number 7559486 (Why is no real title available?)
- Verifiable Code Generation from Scheduled Event-B Models
- Stepwise refinement of heap-manipulating code in Chalice
- Holistic Specifications for Robust Programs
- Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm
- Modular verification of higher-order functional programs
- Executable contracts for Elixir
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
- Theory exploration powered by deductive synthesis
- Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- Formal Reasoning Using Distributed Assertions
- Abstraction and subsumption in modular verification of C programs
- Building Specifications in the Event-B Institution
- Reasoning about algebraic data types with abstractions
- A survey of emerging threats in cybersecurity
- A verification-driven framework for iterative design of controllers
- Verification of the ROS NavFn planner using executable specification languages
- Featherweight VeriFast
- A matching logic foundation for Alk
- A first-order logic with frames
- VST-Floyd: a separation logic tool to verify correctness of C programs
- Embedded domain specific verifiers
- Why3 -- where programs meet provers
- Automated verification of correctness for masked arithmetic programs
- Automatic program instrumentation for automatic verification
- On strings in software model checking
- Synthesis of distributed agreement-based systems with efficiently-decidable verification
- Aneris: a mechanised logic for modular reasoning about distributed systems
- The spirit of ghost code
- The symbiosis of concurrency and verification: teaching and case studies
- Verification of concurrent systems with VerCors
- Compositional reasoning for non-multicopy atomic architectures
- AUSPICE-R: automatic safety-property proofs for realistic features in machine code
Describes a project that uses
Uses Software
This page was built for publication: Dafny: an automatic program verifier for functional correctness
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3066108)
