University of Cambridge > Talks.cam > Computer Laboratory Systems Research Group Seminar > Modeling, Specifying, and Verifying X86 Hardware and Software

Modeling, Specifying, and Verifying X86 Hardware and Software

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Eiko Yoneki.

We describe our work concerning X86 ISA specification and its use in verifying the correctness of the VIA Nano design and for verifying X86 binary programs. Our talk will be three part: a brief description of our tools and methods, our modeling and verification of the VIA Nano, and our verification of X86 binary code. The VIA Nano is a X86 -compatible, 64-bit microprocessor; this processor appears in HP and Lenovo products and in many X86 -based, embedded computers.

We will describe our use of the ACL2 logic to model the X86 ISA and verify binary programs. We give a simple example of verifying a word-count program. We also describe our modeling of the VIA Nano design, and describe our efforts at verifying Nano microcode. Microcode is the heart of modern microprocessors, and it implements some of the most complex processor-internal control functions: it is tightly connected to the machine state, written in an assembly-like language that has no support for data or control structures, and it has ever-changing semantics.

Bio: see http://www.cs.utexas.edu/users/hunt/index.html.

This talk is part of the Computer Laboratory Systems Research Group Seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity