The following pages link to Dafny (Q12950):
Displaying 50 items.
- Automata-theoretic semantics of idealized Algol with passive expressions (Q265826) (← links)
- Contract-based verification of MATLAB-style matrix programs (Q282101) (← links)
- Fundamentals of software engineering. 6th international conference, FSEN 2015, Tehran, Iran, April 22--24, 2015. Revised selected papers (Q497870) (← links)
- The spirit of ghost code (Q518394) (← links)
- Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 -- May 1, 2010. Revised selected papers (Q610791) (← links)
- Building program construction and verification tools from algebraic principles (Q736461) (← links)
- Formal verification of a Java component using the RESOLVE framework (Q831953) (← links)
- Product programs in the wild: retrofitting program verifiers to check information flow security (Q832225) (← links)
- Theory exploration powered by deductive synthesis (Q832255) (← links)
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms (Q832310) (← links)
- Toward compositional verification of interruptible OS kernels and device drivers (Q1663225) (← links)
- VST-Floyd: a separation logic tool to verify correctness of C programs (Q1663238) (← links)
- A formal proof generator from semi-formal proof documents (Q1675786) (← links)
- Reasoning about algebraic data types with abstractions (Q1694026) (← links)
- Deciding local theory extensions via E-matching (Q1702888) (← links)
- The symbiosis of concurrency and verification: teaching and case studies (Q1707345) (← links)
- Backwards and forwards with separation logic (Q1791147) (← links)
- Relational parametricity and quotient preservation for modular (co)datatypes (Q1791181) (← links)
- Towards verified handwritten calculational proofs (short paper) (Q1791183) (← links)
- Unifying separation logic and region logic to allow interoperability (Q1798668) (← links)
- A Why3 framework for reflection proofs and its application to GMP's algorithms (Q1799078) (← links)
- Datatypes with shared selectors (Q1799121) (← links)
- Loop invariant synthesis in a combined abstract domain (Q1930180) (← links)
- Stepwise refinement of heap-manipulating code in Chalice (Q1941869) (← links)
- An assertional proof of red-black trees using Dafny (Q1984797) (← links)
- Alloy*: a general-purpose higher-order relational constraint solver (Q2009609) (← links)
- Quicksort revisited. Verifying alternative versions of quicksort (Q2026813) (← links)
- Real-time solving of computationally hard problems using optimal algorithm portfolios (Q2043446) (← links)
- Simpler proofs with decentralized invariants (Q2043795) (← links)
- Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models (Q2095426) (← links)
- Removing algebraic data types from constrained Horn clauses using difference predicates (Q2096439) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- Inductive benchmarks for automated reasoning (Q2128807) (← links)
- Automated verification of the parallel Bellman-Ford algorithm (Q2145339) (← links)
- Abstraction and subsumption in modular verification of C programs (Q2147702) (← links)
- Verifying the conversion into CNF in dafny (Q2148786) (← links)
- Loop verification with invariants and contracts (Q2152642) (← links)
- Generalized arrays for Stainless frames (Q2152661) (← links)
- Traits: correctness-by-construction for free (Q2165220) (← links)
- A learning-based approach to synthesizing invariants for incomplete verification engines (Q2208307) (← links)
- Indexed and fibred structures for Hoare logic (Q2219084) (← links)
- Loop summarization using state and transition invariants (Q2248058) (← links)
- Fifty years of Hoare's logic (Q2280214) (← links)
- Efficient verification of imperative programs using auto2 (Q2324204) (← links)
- Automating deductive verification for weak-memory programs (Q2324213) (← links)
- A verification-driven framework for iterative design of controllers (Q2335947) (← links)
- Verifying data- and control-oriented properties combining static and runtime verification: theory and tools (Q2402555) (← links)
- Verification of the ROS NavFn planner using executable specification languages (Q2693303) (← links)
- Viper: A Verification Infrastructure for Permission-Based Reasoning (Q2796035) (← links)
- Asynchronous User Interaction and Tool Integration in Isabelle/PIDE (Q2879273) (← links)
