Modeling, Specifying, and Verifying X86 Hardware and Software

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

• Anna Slobodova (Centaur Technology) and Warren Hunt (University of Texas Austin)
• Thursday 31 July 2014, 15:00-16:00
• FW26, Computer Laboratory, William Gates Builiding.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• CL's SRG seminar
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Computer Laboratory Systems Research Group Seminar
• Department of Computer Science and Technology talks and seminars
• FW26, Computer Laboratory, William Gates Builiding
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• rp587

Note that ex-directory lists are not shown.