Certified assembly programming with embedded code pointers

DOI10.1145/1111037.1111066zbMATH Open1369.68150OpenAlexW2165970356MaRDI QIDQ5348933FDOQ5348933

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

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

zbMATH Keywords

Hoare logichigher-order functionsproof-carrying codeembedded code pointers

Mathematics Subject Classification ID

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

Cited In (10)

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

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)