The following pages link to Dafny (Q12950):
Displaying 36 items.
- Decision Procedures for Region Logic (Q2891431) (← links)
- The relationship between separation logic and implicit dynamic frames (Q2904617) (← links)
- Taking Satisfiability to the Next Level with Z3 (Q2908472) (← links)
- Modular Synthesis of Sketches Using Models (Q2938080) (← links)
- (Q2979840) (← links)
- Modular Verification of Higher-Order Functional Programs (Q2988670) (← links)
- Modular Verification of Procedure Equivalence in the Presence of Memory Allocation (Q2988675) (← links)
- The Relationship between Separation Logic and Implicit Dynamic Frames (Q3000593) (← links)
- Enforcing Structural Invariants Using Dynamic Frames (Q3000638) (← links)
- AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code (Q3179279) (← links)
- Ensuring Correctness of Model Transformations While Remaining Decidable (Q3179408) (← links)
- Bounded Quantifier Instantiation for Checking Inductive Invariants (Q3303891) (← links)
- TIP: Tons of Inductive Problems (Q3453129) (← links)
- TIP: Tools for Inductive Provers (Q3460056) (← links)
- Reasoning About Loops Using Vampire in KeY (Q3460073) (← links)
- Principled Software Development (Q4558903) (← links)
- Collaborative Verification and Testing with Explicit Assumptions (Q4647837) (← links)
- Theory and Techniques for Synthesizing Efficient Breadth-First Search Algorithms (Q4647853) (← links)
- One Logic to Use Them All (Q4928425) (← links)
- Synchronizing the asynchronous (Q5009435) (← links)
- Automated Verification of Parallel Nested DFS (Q5039512) (← links)
- Holistic Specifications for Robust Programs (Q5039542) (← links)
- Verifying Visibility-Based Weak Consistency (Q5041095) (← links)
- Local Reasoning for Global Graph Properties (Q5041096) (← links)
- A First-Order Logic with Frames (Q5041109) (← links)
- ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs (Q5041118) (← links)
- Building Specifications in the Event-B Institution (Q5060190) (← links)
- Verification of Concurrent Systems with VerCors (Q5175776) (← links)
- Heaps and Data Structures: A Challenge for Automated Provers (Q5200023) (← links)
- A Verified Theorem Prover Backend Supported by a Monotonic Library (Q5222980) (← links)
- An Assertional Proof of the Stability and Correctness of Natural Mergesort (Q5277907) (← links)
- Automating Theorem Proving with SMT (Q5327333) (← links)
- Dijkstra monads for free (Q5370885) (← links)
- Verifiable Code Generation from Scheduled Event-B Models (Q5881452) (← links)
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker (Q5883751) (← links)
- Indexed and fibered structures for partial and total correctness assertions (Q5889306) (← links)
