Certifying assembly programs with trails

DOI10.1007/S11704-011-0166-ZzbMath1267.68098OpenAlexW2139253383MaRDI QIDQ352100

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

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

Uses Software

• Coq
• TALx86

Cites Work

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

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