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.
CITATION STYLE
Grundy, J. (2000). Verified optimizations for the intel* Ia-64 architecture**. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1869, pp. 215–232). Springer Verlag. https://doi.org/10.1007/3-540-44659-1_14
Mendeley helps you to discover research relevant for your work.