Title: Department of Computer Science Seminar
Date: Wednesday, March 15, 2000
Time: 4:00pm to 5:00 pm
Venue: Room N101, CSIT Building [108]
Speaker: Dr Jim Grundy (Lecturer, DCS at ANU)
Description: "Verified Optimizations for the Intel IA-64 Architecture"


                        Abstract

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

 
URL: http://cs.anu.edu.au/lib/seminars/seminars00/dept20000315