Toolchain

swMATH9517MaRDI QIDQ21498FDOQ21498

Author name not available (Why is that?)

Cited In (38)

• Verifying Whiley programs with Boogie
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
• Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
• Verified cryptographic code for everybody
• Relational Decomposition
• Safe functional systems through integrity types and verified assembly
• On models of higher-order separation logic
• Extensible and Efficient Automation Through Reflective Tactics
• A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
• A complete semantics of \(\mathbb{K}\) and its translation to Isabelle
• Bringing Order to the Separation Logic Jungle
• AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow
• The Essence of Higher-Order Concurrent Separation Logic
• Verified Characteristic Formulae for CakeML
• Transfinite Step-Indexing: Decoupling Concrete and Logical Steps
• Effect algebras, Girard quantales and complementation in separation logic
• System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
• Title not available (Why is that?)
• Towards a Unified Theory of Operational and Axiomatic Semantics
• Connecting Higher-Order Separation Logic to a First-Order Outside World
• Formally verifying exceptions for low-level code with separation logic
• Abstraction and subsumption in modular verification of C programs
• All-Path Reachability Logic
• A formal C memory model for separation logic
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Featherweight VeriFast
• From Hoare Logic to Matching Logic Reachability
• Verified Software Toolchain
• Towards patterns for heaps and imperative lambdas
• Temporary Read-Only Permissions for Separation Logic
• Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
• Local Reasoning for Global Graph Properties
• VST-Floyd: a separation logic tool to verify correctness of C programs
• From Rewriting Logic, to Programming Language Semantics, to Program Verification
• Program Logics for Certified Compilers

This page was built for software: Toolchain