Dafny
From MaRDI portal
Software:12950
No author found.
Related Items (86)
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 ⋮ 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 ⋮ Decision Procedures for Region Logic ⋮ Unnamed Item ⋮ Formal verification of a Java component using the RESOLVE framework ⋮ 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 ⋮ TIP: Tons of Inductive Problems ⋮ The Relationship Between Separation Logic and Implicit Dynamic Frames ⋮ AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code ⋮ Ensuring Correctness of Model Transformations While Remaining Decidable ⋮ Automated verification of the parallel Bellman-Ford algorithm ⋮ Taking Satisfiability to the Next Level with Z3 ⋮ Building Specifications in the Event-B Institution ⋮ Abstraction and subsumption in modular verification of C programs ⋮ TIP: Tools for Inductive Provers ⋮ Reasoning About Loops Using Vampire in KeY ⋮ Verifying the conversion into CNF in dafny ⋮ Loop verification with invariants and contracts ⋮ Generalized arrays for Stainless frames ⋮ Principled Software Development ⋮ 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 ⋮ Automating Theorem Proving with SMT ⋮ Modular Synthesis of Sketches Using Models ⋮ A formal proof generator from semi-formal proof documents ⋮ Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 -- May 1, 2010. Revised selected papers ⋮ Loop invariant synthesis in a combined abstract domain ⋮ Reasoning about algebraic data types with abstractions ⋮ Stepwise refinement of heap-manipulating code in Chalice ⋮ Verification of the ROS NavFn planner using executable specification languages ⋮ Deciding local theory extensions via E-matching ⋮ Unnamed Item ⋮ The symbiosis of concurrency and verification: teaching and case studies ⋮ Dijkstra monads for free ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ Indexed and fibred structures for Hoare 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 ⋮ Fundamentals of software engineering. 6th international conference, FSEN 2015, Tehran, Iran, April 22--24, 2015. Revised selected papers ⋮ An assertional proof of red-black trees using Dafny ⋮ Collaborative Verification and Testing with Explicit Assumptions ⋮ Theory and Techniques for Synthesizing Efficient Breadth-First Search Algorithms ⋮ 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 ⋮ One Logic to Use Them All ⋮ Quicksort revisited. Verifying alternative versions of quicksort ⋮ Fifty years of Hoare's logic ⋮ Heaps and Data Structures: A Challenge for Automated Provers ⋮ Viper: A Verification Infrastructure for Permission-Based Reasoning ⋮ Backwards and forwards with separation logic ⋮ Relational parametricity and quotient preservation for modular (co)datatypes ⋮ Towards verified handwritten calculational proofs (short paper) ⋮ Unifying separation logic and region logic to allow interoperability ⋮ A Why3 framework for reflection proofs and its application to GMP's algorithms ⋮ Datatypes with shared selectors ⋮ 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 ⋮ A Verified Theorem Prover Backend Supported by a Monotonic Library ⋮ Efficient verification of imperative programs using auto2 ⋮ Automating deductive verification for weak-memory programs ⋮ 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 ⋮ Removing algebraic data types from constrained Horn clauses using difference predicates ⋮ Verifying Whiley programs with Boogie ⋮ Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
This page was built for software: Dafny
