scientific article; zbMATH DE number 1956565

MaRDI QIDQ4417905zbMATH OpenFDO

Authors Dachuan Yu, Nadeem A. Hamid, Zhong Shao

Publication date 30 July 2003

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
• scientific article; zbMATH DE number 1962754
• Proof-carrying code from certified abstract interpretation and fixpoint compression
• scientific article; zbMATH DE number 2090287
• 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:

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