Certifying assembly programs with trails

DOI10.1007/S11704-011-0166-ZMaRDI QIDQ352100zbMATH OpenOpenAlexFDO

Authors Wei Wang

Publication date 4 July 2013

Published in Frontiers of Computer Science in China (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11704-011-0166-z

zbMATH Keywords

partial correctnesscertifying assembly codecontrol flow

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 1953021
• Certified assembly programming with embedded code pointers
• Certifying compilation and run-time code generation
• scientific article; zbMATH DE number 1746459
• scientific article; zbMATH DE number 1956568

Cites work

• An axiomatic basis for computer programming
• CFA2: A Context-Free Approach to Control-Flow Analysis
• Certified assembly programming with embedded code pointers
• Stack-based typed assembly language
• Tentative steps toward a development method for interfering programs
• Verification, Model Checking, and Abstract Interpretation

Cited in

(1)

• scientific article; zbMATH DE number 1953021 (Why is no real title available?)

Describes a project that uses

Uses Software

• TALx86
• Coq

This page was built for publication: Certifying assembly programs with trails

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