Toolchain

swMATH9517MaRDI QIDQ21498FDOQ21498

Author name not available (Why is that?)

Cited In (38)

• Verifying Whiley programs with Boogie
• Connecting higher-order separation logic to a first-order outside world
• 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
• Safe functional systems through integrity types and verified assembly
• On models of higher-order separation logic
• A certificate infrastructure for machine-checked proofs of conditional information flow
• All-path reachability logic
• 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
• Verified characteristic formulae for CakeML
• The essence of higher-order concurrent separation logic
• Transfinite step-indexing: decoupling concrete and logical steps
• Bringing Order to the Separation Logic Jungle
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Program logics for certified compilers
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Towards a unified theory of operational and axiomatic semantics
• From hoare logic to matching logic reachability
• Concise read-only specifications for better synthesis of programs with pointers
• Local reasoning for global graph properties
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• 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?)
• Verified software toolchain (invited talk)
• Temporary read-only permissions for separation logic
• From rewriting logic, to programming language semantics, to program verification
• Formally verifying exceptions for low-level code with separation logic
• Relational decomposition
• Abstraction and subsumption in modular verification of C programs
• A formal C memory model for separation logic
• Featherweight VeriFast
• Towards patterns for heaps and imperative lambdas
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Extensible and efficient automation through reflective tactics
• AUSPICE-R: automatic safety-property proofs for realistic features in machine code

This page was built for software: Toolchain