Dafny: An Automatic Program Verifier for Functional Correctness

DOI10.1007/978-3-642-17511-4_20zbMath1253.68095OpenAlexW2130427425MaRDI QIDQ3066108

Publication date: 7 January 2011

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-17511-4_20

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (76)

Automata-theoretic semantics of idealized Algol with passive expressions ⋮ Verifiable Code Generation from Scheduled Event-B Models ⋮ An Assertional Proof of the Stability and Correctness of Natural Mergesort ⋮ Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker ⋮ Automated Verification of Parallel Nested DFS ⋮ Holistic Specifications for Robust Programs ⋮ Contract-based verification of MATLAB-style matrix programs ⋮ Verifying Visibility-Based Weak Consistency ⋮ Local Reasoning for Global Graph Properties ⋮ Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems ⋮ A First-Order Logic with Frames ⋮ ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs ⋮ Indexed and fibered structures for partial and total correctness assertions ⋮ Inductive benchmarks for automated reasoning ⋮ Automating Induction with an SMT Solver ⋮ Decision Procedures for Region Logic ⋮ Product programs in the wild: retrofitting program verifiers to check information flow security ⋮ Theory exploration powered by deductive synthesis ⋮ Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms ⋮ AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code ⋮ Ensuring Correctness of Model Transformations While Remaining Decidable ⋮ Building Specifications in the Event-B Institution ⋮ 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 ⋮ Toward compositional verification of interruptible OS kernels and device drivers ⋮ VST-Floyd: a separation logic tool to verify correctness of C programs ⋮ Verifying data- and control-oriented properties combining static and runtime verification: theory and tools ⋮ Regular model checking revisited ⋮ Trace-based verification of imperative programs with I/O ⋮ 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 ⋮ Reasoning about algebraic data types with abstractions ⋮ Flexible Correct-by-Construction Programming ⋮ Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ Towards a dereversibilizer: fewer asserts, statically ⋮ Stepwise refinement of heap-manipulating code in Chalice ⋮ 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 ⋮ 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 ⋮ Verification of the ROS NavFn planner using executable specification languages ⋮ Unnamed Item ⋮ The symbiosis of concurrency and verification: teaching and case studies ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ A survey of emerging threats in cybersecurity ⋮ Indexed and fibred structures for Hoare logic ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation 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 ⋮ Bounded Quantifier Instantiation for Checking Inductive Invariants ⋮ An assertional proof of red-black trees using Dafny ⋮ The spirit of ghost code ⋮ Loop summarization using state and transition invariants ⋮ Verification of Concurrent Systems with VerCors ⋮ Alloy*: a general-purpose higher-order relational constraint solver ⋮ Unnamed Item ⋮ Heaps and Data Structures: A Challenge for Automated Provers ⋮ Unifying separation logic and region logic to allow interoperability ⋮ Building program construction and verification tools from algebraic principles ⋮ Real-time solving of computationally hard problems using optimal algorithm portfolios ⋮ Simpler proofs with decentralized invariants ⋮ Certified abstract cost analysis ⋮ Dafny ⋮ A verification-driven framework for iterative design of controllers ⋮ Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models ⋮ Verifying Whiley programs with Boogie ⋮ Cogent: uniqueness types and certifying compilation

Uses Software

This page was built for publication: Dafny: An Automatic Program Verifier for Functional Correctness