Pages that link to "Item:Q3066108"
From MaRDI portal
The following pages link to Dafny: An Automatic Program Verifier for Functional Correctness (Q3066108):
Displaying 50 items.
- Dafny (Q12950) (← links)
- Automata-theoretic semantics of idealized Algol with passive expressions (Q265826) (← links)
- Contract-based verification of MATLAB-style matrix programs (Q282101) (← links)
- The spirit of ghost code (Q518394) (← links)
- Trace-based verification of imperative programs with I/O (Q617977) (← links)
- Building program construction and verification tools from algebraic principles (Q736461) (← 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)
- Reasoning about algebraic data types with abstractions (Q1694026) (← links)
- The symbiosis of concurrency and verification: teaching and case studies (Q1707345) (← links)
- Unifying separation logic and region logic to allow interoperability (Q1798668) (← 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)
- Real-time solving of computationally hard problems using optimal algorithm portfolios (Q2043446) (← links)
- Simpler proofs with decentralized invariants (Q2043795) (← links)
- Certified abstract cost analysis (Q2044174) (← links)
- Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models (Q2095426) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- Inductive benchmarks for automated reasoning (Q2128807) (← links)
- Abstraction and subsumption in modular verification of C programs (Q2147702) (← 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)
- 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)
- A survey of emerging threats in cybersecurity (Q2442167) (← links)
- Verification of the ROS NavFn planner using executable specification languages (Q2693303) (← links)
- Automating Induction with an SMT Solver (Q2891425) (← links)
- Decision Procedures for Region Logic (Q2891431) (← 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)
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic (Q4625160) (← links)
- (Q5009435) (← links)
- Cogent: uniqueness types and certifying compilation (Q5019022) (← 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)
