How can you trust formally verified software?

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

• Alastair Reid, ARM
• Tuesday 02 May 2017, 13:15-14:15
• FW26, Computer Laboratory.

If you have a question about this talk, please contact Jan Samols.

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.

This talk is part of the Technical Talks - Department of Computer Science and Technology series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Department of Computer Science and Technology talks and seminars
• FW26, Computer Laboratory
• Guy Emerson's list
• Interested Talks
• School of Technology
• Technical Talks - Department of Computer Science and Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• rp587

Note that ex-directory lists are not shown.