Automated proofs of object code for a widely used microprocessor

DOI10.1145/227595.227603MaRDI QIDQ4371519zbMATH OpenOpenAlexWikidataFDO

Authors Robert S. Boyer, Yuan Yu

Publication date 19 January 1998

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL http://www.acm.org/pubs/contents/journals/jacm/1996-43/

zbMATH Keywords

automated reasoningGnu Common Lips compilers

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 1696819
• scientific article; zbMATH DE number 53982
• Formal modeling and verification of microprocessors
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor

Cited in

(8)

• Mechanical certification of systolic algorithms
• Parameterized synthesis for fragments of first-order logic over data words
• scientific article; zbMATH DE number 1696819 (Why is no real title available?)
• Hardware-Dependent Proofs of Numerical Programs
• scientific article; zbMATH DE number 4074538 (Why is no real title available?)
• Function extraction
• Highly automated formal proofs over memory usage of assembly code
• A mechanical analysis of program verification strategies

Describes a project that uses

Uses Software

• LCF

This page was built for publication: Automated proofs of object code for a widely used microprocessor

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