Abstract

Formal verification of software has finally started to become viable: we have examples of formally verified realistic compilers, operating systems, hypervisors etc. These are huge achievements and we can expect to see even more impressive results in the future but these proofs depend on a number of assumptions about the environment the code must work in. One of the biggest assumptions involves the hardware on which the verified programs must run: Are they verified against a correct specification? Are the processors themselves correct? This talk will describe the combination of formal verification and testing that we are applying to the ARM specification and how we can use this specification to formally verify processors. It will focus on our current challenge: getting the specification down to zero bugs while the architecture continues to evolve.

Bio: Alastair Reid is a Senior Principal Research Engineer at ARM Ltd. His current research focus is on formalizing the ARM architecture specifications and finding ways that those specifications can be used to make hardware and software better. He has 16 granted patents in Computer Architecture and is the author of over a dozen research papers in Formal Verification, Software Defined Radio, Operating Systems, and Lazy Functional Programming. In his spare time, he builds his own keyboards and enjoys trashing his body in cyclocross races.