Program Logics for Certified Compilers
From MaRDI portal
Publication:5494381
DOI10.1017/CBO9781107256552zbMath1298.68009OpenAlexW564852913MaRDI QIDQ5494381
Robert Dockins, Sandrine Blazy, Andrew W. Appel, Aquinas Hobor, Gordon Stewart, Josiah Dodds, Xavier Leroy, Lennart Beringer
Publication date: 28 July 2014
Full work available at URL: https://doi.org/10.1017/cbo9781107256552
Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Connecting Higher-Order Separation Logic to a First-Order Outside World, On models of higher-order separation logic, 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, Towards patterns for heaps and imperative lambdas, Bringing Order to the Separation Logic Jungle, Abstraction and subsumption in modular verification of C programs, Certified compilation for cryptography: extended x86 instructions and constant-time verification, 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, Efficient extensional binary tries, Unnamed Item, Effect algebras, Girard quantales and complementation in separation logic, Iris from the ground up: A modular foundation for higher-order concurrent separation logic, 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 units, Strong-separation logic, A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data, Unnamed Item, Extensible and Efficient Automation Through Reflective Tactics, Transfinite Step-Indexing: Decoupling Concrete and Logical Steps, Verifying Whiley programs with Boogie, A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
Uses Software
