Dafny

swMATH183MaRDI QIDQ12950FDOQ12950

Author name not available (Why is that?)

Described by source

• Automating Induction with an SMT Solver
• Dafny: An Automatic Program Verifier for Functional Correctness

Cited In (86)

• Loop summarization using state and transition invariants
• An assertional proof of red-black trees using Dafny
• Heaps and Data Structures: A Challenge for Automated Provers
• Verifying Whiley programs with Boogie
• Automata-theoretic semantics of idealized Algol with passive expressions
• 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
• Efficient verification of imperative programs using auto2
• TIP: Tools for Inductive Provers
• Contract-based verification of MATLAB-style matrix programs
• Alloy*: a general-purpose higher-order relational constraint solver
• AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code
• The Relationship between Separation Logic and Implicit Dynamic Frames
• Fifty years of Hoare's logic
• Simpler proofs with decentralized invariants
• A Verified Theorem Prover Backend Supported by a Monotonic Library
• Building program construction and verification tools from algebraic principles
• One Logic to Use Them All
• Quicksort revisited. Verifying alternative versions of quicksort
• Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
• Automating deductive verification for weak-memory programs
• Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
• Taking Satisfiability to the Next Level with Z3
• Automated verification of the parallel Bellman-Ford algorithm
• Verifying the conversion into CNF in dafny
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• Real-time solving of computationally hard problems using optimal algorithm portfolios
• Toward compositional verification of interruptible OS kernels and device drivers
• Verification of Concurrent Systems with VerCors
• Deciding local theory extensions via E-matching
• Backwards and forwards with separation logic
• Relational parametricity and quotient preservation for modular (co)datatypes
• Towards verified handwritten calculational proofs (short paper)
• Theory and Techniques for Synthesizing Efficient Breadth-First Search Algorithms
• Inductive benchmarks for automated reasoning
• Bounded Quantifier Instantiation for Checking Inductive Invariants
• TIP: Tons of Inductive Problems
• A Why3 framework for reflection proofs and its application to GMP's algorithms
• Unifying separation logic and region logic to allow interoperability
• Datatypes with shared selectors
• An Assertional Proof of the Stability and Correctness of Natural Mergesort
• Stepwise refinement of heap-manipulating code in Chalice
• Loop invariant synthesis in a combined abstract domain
• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• Theory exploration powered by deductive synthesis
• Title not available (Why is that?)
• Abstraction and subsumption in modular verification of C programs
• Fundamentals of software engineering. 6th international conference, FSEN 2015, Tehran, Iran, April 22--24, 2015. Revised selected papers
• Collaborative Verification and Testing with Explicit Assumptions
• A verification-driven framework for iterative design of controllers
• Reasoning about algebraic data types with abstractions
• Local Reasoning for Global Graph Properties
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Decision Procedures for Region Logic
• The relationship between separation logic and implicit dynamic frames
• Automated Verification of Parallel Nested DFS
• The symbiosis of concurrency and verification: teaching and case studies
• The spirit of ghost code
• Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 -- May 1, 2010. Revised selected papers
• Dijkstra monads for free
• A formal proof generator from semi-formal proof documents
• Removing algebraic data types from constrained Horn clauses using difference predicates
• Modular Verification of Higher-Order Functional Programs
• A learning-based approach to synthesizing invariants for incomplete verification engines
• Indexed and fibred structures for Hoare logic
• ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
• Reasoning About Loops Using Vampire in KeY
• Ensuring Correctness of Model Transformations While Remaining Decidable
• Modular Synthesis of Sketches Using Models
• Indexed and fibered structures for partial and total correctness assertions
• A First-Order Logic with Frames
• Generalized arrays for Stainless frames
• Loop verification with invariants and contracts
• Traits: correctness-by-construction for free
• Verifiable Code Generation from Scheduled Event-B Models
• Holistic Specifications for Robust Programs
• Enforcing Structural Invariants Using Dynamic Frames
• Principled Software Development
• Verifying Visibility-Based Weak Consistency
• Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
• Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
• Building Specifications in the Event-B Institution
• Verification of the ROS NavFn planner using executable specification languages
• Automating Theorem Proving with SMT
• Title not available (Why is that?)

This page was built for software: Dafny