Verified Optimizations for the Intel IA-64 Architecture

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.

• Type: Conference
• Year: 2000
• Where: TPHOL
• Authors: Jim Grundy
• Keywords: Assembly-level Code Optimizations, Automated Reasoning, HOL Light Theorem Prover, Intel IA-64 Architecture, TPHOL 2000