A tutorial example of the semantic approach to foundational proof-carrying code

DOI10.1007/978-3-540-32033-3_29MaRDI QIDQ5703864zbMATH OpenOpenAlexFDO

Authors Amy P. Felty

Publication date 11 November 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b135673

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Semantics in the theory of computing (68Q55)

Recommendations

• Tutorial examples of the semantic approach to foundational proof-carrying code
• A tutorial example of the semantic approach to foundational proof-carrying code: Abstract
• A syntactic approach to foundational proof-carrying code
• A gradual approach to a more trustworthy, yet scalable, proof-carrying code
• scientific article; zbMATH DE number 2110618

Cited in

(12)

• A syntactic approach to foundational proof-carrying code
• Reasoning about a machine with local capabilities. Provably safe stack and return pointer management
• Machine instruction syntax and semantics in higher order logic
• Tutorial examples of the semantic approach to foundational proof-carrying code
• Proof-carrying code with untrusted proof rules
• A gradual approach to a more trustworthy, yet scalable, proof-carrying code
• A semantic model of types and machine instructions for proof-carrying code
• Foundational certified code in the Twelf metalogical framework
• Certified assembly programming with embedded code pointers
• Interfacing Hoare logic and type systems for foundational proof-carrying code
• A tutorial example of the semantic approach to foundational proof-carrying code: Abstract
• Automatic construction of Hoare proofs from abstract interpretation results.

This page was built for publication: A tutorial example of the semantic approach to foundational proof-carrying code

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