The unforeseen evolution of theorem proving in ARM processor verification
4.00pm, Tuesday 28th April 2015
Robert Recorde Room, Faraday Buidling (Level 2), Swansea University
The presented slides and an accompanying report are available
The lecture will tell the story of how a research project to verify an ARM processor changed direction and focus over fifteen years.
The project was initially joint with Leeds and Cambridge universities. Leeds' goal was to specify the ARM instruction set and the ARM610 microprocessor. Cambridge's goal was to use automated theorem proving to verify that the processor correctly implemented ARM instructions. The experience gained from this project resulted in changed priorities for subsequent research. New methods for coupling processor specifications to theorem proving tools emerged and the goals expanded to include software verification. Eventually the work started to find applications at Cambridge and elsewhere. These applications range from proving properties of operating system machine code to exploring new security enhanced processor designs.
The talk is intended for a general audience. No knowledge of formal verification or theorem proving will be assumed.
Mike Gordon is a member of the University of Cambridge Computer Laboratory. In 1970 he graduated BA (mathematics) from Gonville & Caius College Cambridge; in 1973 he obtained a PhD from the University of Edinburgh, supervised by Rod Burstall, and in 1974 a Diploma in Linguistics from King’s College Cambridge. In 1974 he started his first job, a research assistant to John McCarthy at the Stanford Artificial Intelligence Laboratory. In 1975 he returned to Edinburgh as a research assistant to Robin Milner on the LCF project. In 1981 he was appointed Lecturer at Cambridge and in 1996 was promoted to Professor. He was elected Fellow of The Royal Society in 1994. Gordon’s research has applied computer assisted reasoning to both hardware and software verification.