High-level separation logic for low-level code

DOI10.1145/2429069.2429105MaRDI QIDQ2931805zbMATH OpenOpenAlexWikidataFDO

Authors Jonas Braband Jensen, Nick Benton, Andrew Kennedy

Publication date 27 November 2014

Published in Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2429069.2429105

zbMATH Keywords

separation logicmachine codeproof assistants

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• Separation Logic for Higher-Order Store
• Hoare Logic for Realistically Modelled Machine Code
• A Simple Model of Separation Logic for Higher-Order Store
• Computer Science Logic
• Types, Maps and Separation Logic

Cited in

(12)

• Verified abstract interpretation techniques for disassembling low-level self-modifying code
• Fully abstract trace semantics for protected module architectures
• Improved tool support for machine-code decompilation in HOL4
• Hoare-style logic for unstructured programs
• A compositional natural semantics and Hoare logic for low-level languages
• Hoare Logic for Realistically Modelled Machine Code
• Temporary read-only permissions for separation logic
• Formally verifying exceptions for low-level code with separation logic
• Hoare Logic for ARM Machine Code
• Frame rules from answer types for code pointers
• Separation logic for non-local control flow and block scope variables
• Types, Maps and Separation Logic

Describes a project that uses

Uses Software

• Coq

This page was built for publication: High-level separation logic for low-level code

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2931805)