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 a year in the Department of Computer Science of Åbo Akademi University in Finland, returned to Cambridge as a Research Associate working on Floating Point Verification.

He has helped to organize several major computer science conferences, most recently the IEEE ARITH (computer arithmetic) conference in Portland, OR. He is a regular participant in a wide range of academic events, and is the author of the recently published textbook "Handbook of Practical Logic and Automated Reasoning". He is a member of the editorial board of the Journal of Automated Reasoning.

For more details, visit his home page.