BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Modeling\, Specifying\, and Verifying X86 Hardware and Software - 
 Anna Slobodova (Centaur Technology) and Warren Hunt (University of Texas A
 ustin)
DTSTART:20140731T140000Z
DTEND:20140731T150000Z
UID:TALK53555@talks.cam.ac.uk
CONTACT:Eiko Yoneki
DESCRIPTION: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\, an
 d 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.\n\nWe will describe our use of
  the ACL2 logic to model the\nX86 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 N
 ano microcode.\nMicrocode 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.\n\nBio: see http://www.cs.utexas.edu/users/hunt/i
 ndex.html. 
LOCATION:FW26\, Computer Laboratory\, William Gates Builiding
END:VEVENT
END:VCALENDAR