Toolchain

swMATH9517MaRDI QIDQ21498

No author found.

Related Items (38)

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

This page was built for software: Toolchain