Science and Technology Seminar

Date: 28/10/2013 Time: 15:00-16:00 Location: TBA

Speaker: John Harrison (Intel Corporation)

Title: Opportunities and Challenges for Automated Reasoning


The capabilities of automated reasoning systems are improving steadily. They are already being applied in a wide variety of areas. Two of the most important applications are formal verification of computer systems in a broad sense (software, hardware, protocols, algorithms) and the formalization of mathematical proofs. In both these areas they are helping to address real problems, and we will give some examples including formal verification activities at Intel, and the Flyspeck project to formalize Hales’s proof of the Kepler conjecture. However, such challenging applications bring problems, including the difficulty of integrating multiple reasoning tools and in handling highly intuitive geometrical reasoning. We will outline some interesting possibilities for addressing such issues.

Brief Bio: John Harrison does formal verification at Intel Corporation. He has mainly specialized in verification of floating-point algorithms and other mathematical software, but he is interested in all aspects of theorem proving and verification. He is also interested in floating-point arithmetic itself, and contributed to the revision process that led to the new IEEE 754 floating-point standard. Before joining Intel in 1998, he was a member of the Automated Reasoning Group at the Computer Laboratory of the University of Cambridge. He worked as a Research Associate and PhD student there, supervised by Mike Gordon, and after a spending year in the Department of Computer Science of Aabo Akademi University in Finland, returned to Cambridge as a Research Associate working on Floating Point Verification. He is the author of the recent textbook “Handbook of Practical Logic and Automated Reasoning”.