Certified assembly programming with embedded code pointers

DOI10.1145/1111037.1111066MaRDI QIDQ5348933zbMATH OpenOpenAlexFDO

Authors Zhaozhong Ni, Zhong Shao

Publication date 21 August 2017

Published in Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

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

zbMATH Keywords

embedded code pointershigher-order functionsHoare logicproof-carrying code

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Term Rewriting and Applications
• Building certified libraries for PCC: dynamic storage allocation
• scientific article; zbMATH DE number 2110618
• scientific article; zbMATH DE number 1956565
• Tutorial examples of the semantic approach to foundational proof-carrying code

Cited in

(11)

• On models of higher-order separation logic
• Symbolic execution proofs for higher order store programs
• Crowfoot: A Verifier for Higher-Order Store Programs
• Specification patterns and proofs for recursion through the store
• Certifying assembly programs with trails
• Specification patterns for reasoning about recursion through the store
• Function extraction
• Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
• Hoare-style logic for unstructured programs
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
• A compositional natural semantics and Hoare logic for low-level languages

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Certified assembly programming with embedded code pointers

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