Dafny
From MaRDI portal
Software:12950
swMATH183MaRDI QIDQ12950FDOQ12950
Author name not available (Why is that?)
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