BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:How can you trust formally verified software? - Alastair Reid\, AR
 M
DTSTART:20170502T121500Z
DTEND:20170502T131500Z
UID:TALK72325@talks.cam.ac.uk
CONTACT:Jan Samols
DESCRIPTION:Formal verification of software has finally started to become 
 viable: we have examples of formally verified realistic compilers\, operat
 ing systems\, hypervisors etc. These are huge achievements and we can expe
 ct to see even more impressive results in the future but these proofs depe
 nd on a number of assumptions about the environment the code must work in.
  One of the biggest assumptions involves the hardware on which the verifie
 d programs must run: Are they verified against a correct specification? Ar
 e the processors themselves correct? This talk will describe the combinati
 on of formal verification and testing that we are applying to the ARM spec
 ification and how we can use this specification to formally verify process
 ors. It will focus on our current challenge: getting the specification dow
 n to zero bugs while the architecture continues to evolve.\n\nBio: Alastai
 r Reid is a Senior Principal Research Engineer at ARM Ltd. His current res
 earch focus is on formalizing the ARM architecture specifications and find
 ing ways that those specifications can be used to make hardware and softwa
 re better. He has 16 granted patents in Computer Architecture and is the a
 uthor of over a dozen research papers in Formal Verification\, Software De
 fined Radio\, Operating Systems\, and Lazy Functional Programming.  In his
  spare time\, he builds his own keyboards and enjoys trashing his body in 
 cyclocross races.\n
LOCATION:FW26\, Computer Laboratory
END:VEVENT
END:VCALENDAR