Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

10

TPHOL
2000
IEEE

favoriteEmaildiscussreport

128views Automated Reasoning» more TPHOL 2000»

Verified Optimizations for the Intel IA-64 Architecture

13 years 8 months ago

Verified Optimizations for the Intel IA-64 Architecture

Download www.student.cs.uwaterloo.ca

This paper outlines a formal model of the Intel IA-64 architecture, and explains how this model can be used to verify the correctness of assembly-level code optimizations. The formalization and proofs were carried out using the HOL Light theorem prover.

Jim Grundy

Real-time Traffic

Assembly-level Code Optimizations | Automated Reasoning | HOL Light Theorem Prover | Intel IA-64 Architecture | TPHOL 2000 |

claim paper

Related Content

» Formal Verification of Floating Point Trigonometric Functions

» Formal verification of iterative algorithms in microprocessors

» A CBased RTL Design Verification Methodology for Complex Microprocessor

Post Info
More Details (n/a)

Added	25 Aug 2010
Updated	25 Aug 2010
Type	Conference
Year	2000
Where	TPHOL
Authors	Jim Grundy

Comments (0)