Research exposition (monographs, survey articles) pertaining to computer science (68-02) Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Recommendations
Cited in
(39)- VST-Floyd: a separation logic tool to verify correctness of C programs
- Formally verifying exceptions for low-level code with separation logic
- A formal C memory model for separation logic
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- Verifying Whiley programs with Boogie
- On models of higher-order separation logic
- Abstraction and subsumption in modular verification of C programs
- Certified compilation for cryptography: extended x86 instructions and constant-time verification
- System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
- Verified software units
- Strong-separation logic
- Towards patterns for heaps and imperative lambdas
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- Effect algebras, Girard quantales and complementation in separation logic
- Extensible and efficient automation through reflective tactics
- Transfinite step-indexing: decoupling concrete and logical steps
- The essence of higher-order concurrent separation logic
- Practical Tactics for Separation Logic
- Separation Logic for Small-Step cminor
- Formal system verification. State-of the-art and future trends
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Linear capabilities for fully abstract compilation of separation-logic-verified code
- Connecting higher-order separation logic to a first-order outside world
- Bringing Order to the Separation Logic Jungle
- \textbf{Actris 2.0}: asynchronous session-type based reasoning in separation logic
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- Challenges of software verification. Contributions of the first workshop, CSV, Venice, Italy, May 20, 2022
- Efficient extensional binary tries
- Verified Erasure Correction in Coq with MathComp and VST
- Abstraction and subsumption in modular verification of C programs
- A generalised union of rely-guarantee and separation logic using permission algebras
- Modular verification of intrusive list and tree data structures in separation logic
- Touring the MetaCoq project
- Beyond symbolic heaps: deciding separation logic with inductive definitions
- A mechanized first-order theory of algebraic data types with pattern matching
- A two-level linear dependent type theory
- 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
This page was built for publication: Program logics for certified compilers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5494381)
