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
- Theory and techniques for synthesizing efficient breadth-first search algorithms
- 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
- Modular verification of procedure equivalence in the presence of memory allocation
- Synchronizing the asynchronous
- Taking satisfiability to the next level with Z3 (abstract)
- Contract-based verification of MATLAB-style matrix programs
- Alloy*: a general-purpose higher-order relational constraint solver
- The relationship between separation logic and implicit dynamic frames
- Collaborative verification and testing with explicit assumptions
- Fifty years of Hoare's logic
- TIP: tons of inductive problems
- Viper: a verification infrastructure for permission-based reasoning
- Bounded quantifier instantiation for checking inductive invariants
- Local reasoning for global graph properties
- Automated verification of parallel nested DFS
- Simpler proofs with decentralized invariants
- Building program construction and verification tools from algebraic principles
- Quicksort revisited. Verifying alternative versions of quicksort
- Automating deductive verification for weak-memory programs
- Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
- Automated verification of the parallel Bellman-Ford algorithm
- Verifying the conversion into CNF in dafny
- Real-time solving of computationally hard problems using optimal algorithm portfolios
- Toward compositional verification of interruptible OS kernels and device drivers
- 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)
- Inductive benchmarks for automated reasoning
- Decision procedures for region logic
- 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
- Stepwise refinement of heap-manipulating code in Chalice
- Loop invariant synthesis in a combined abstract domain
- A verified theorem prover backend supported by a monotonic library
- Modular verification of higher-order functional programs
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
- Theory exploration powered by deductive synthesis
- One logic to use them all
- Abstraction and subsumption in modular verification of C programs
- TIP: tools for inductive provers
- Fundamentals of software engineering. 6th international conference, FSEN 2015, Tehran, Iran, April 22--24, 2015. Revised selected papers
- A verification-driven framework for iterative design of controllers
- Reasoning about algebraic data types with abstractions
- VST-Floyd: a separation logic tool to verify correctness of C programs
- The relationship between separation logic and implicit dynamic frames
- Verification of concurrent systems with VerCors
- 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
- AUSPICE-R: automatic safety-property proofs for realistic features in machine code
- A formal proof generator from semi-formal proof documents
- Removing algebraic data types from constrained Horn clauses using difference predicates
- An assertional proof of the stability and correctness of Natural Mergesort
- A learning-based approach to synthesizing invariants for incomplete verification engines
- Indexed and fibred structures for Hoare logic
- Modular synthesis of sketches using models
- Verifying visibility-based weak consistency
- Automating theorem proving with SMT
- Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018
- Two-level mixed verification method of C-light programs in terms of safety logic
- Indexed and fibered structures for partial and total correctness assertions
- Enforcing structural invariants using dynamic frames
- Generalized arrays for Stainless frames
- Loop verification with invariants and contracts
- Asynchronous user interaction and tool integration in Isabelle/PIDE
- ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
- Traits: correctness-by-construction for free
- Verifiable Code Generation from Scheduled Event-B Models
- Holistic Specifications for Robust Programs
- Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- Reasoning about loops using Vampire in KeY
- Building Specifications in the Event-B Institution
- Verification of the ROS NavFn planner using executable specification languages
- A first-order logic with frames
- Ensuring correctness of model transformations while remaining decidable
This page was built for software: Dafny
