Building certified libraries for PCC: Dynamic storage allocation

DOI10.1007/3-540-36575-3_25MaRDI QIDQ4417905zbMATH OpenFDO

Authors Dachuan Yu, Nadeem A. Hamid, Zhong Shao

Publication date 30 July 2003

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2618/26180363.htm

Mathematics Subject Classification ID

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

Recommendations

• Building certified libraries for PCC: dynamic storage allocation
• Proof-carrying code with untrusted proof rules
• Proof-carrying code from certified abstract interpretation and fixpoint compression
• A gradual approach to a more trustworthy, yet scalable, proof-carrying code
• scientific article; zbMATH DE number 2110618

Cited in

(6)

• Building certified libraries for PCC: dynamic storage allocation
• Safe functional systems through integrity types and verified assembly
• Certified assembly programming with embedded code pointers
• A verified specification of TLSF memory management allocator using state monads
• Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
• Hoare-style logic for unstructured programs

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Building certified libraries for PCC: Dynamic storage allocation

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