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