My research interests concern the development of formal verification tools and their application in such areas as hardware verification, software verification, systems biology and formalised mathematics. Specific current interests include the formal verification of hybrid systems (e.g. cyber-physical systems) by the use of deductive theorem proving techniques; automatic proof procedures for non-linear arithmetic; and software verification by the use of verification condition generation and SMT solvers.

1995, PhD in Computer Science, Cornell University
1990, MS in Computer Science, Cornell University
1988, MS in Physics, Cornell University
1984, First class degree in Engineering and Electrical Sciences

Paul Jackson studied Engineering and Electrical Sciences as an undergraduate at the University of Cambridge, graduating in 1984. After designing semi-custom integrated circuits for two years at US General Electric, he returned to academic studies at Cornell University, completing a Masters degree in Physics in 1998 and a PhD in Computer Science in 1995. His PhD research was on the development of the Nuprl interactive theorem proving system and its application to computational abstract algebra, under the supervision of Prof Robert Constable.

Since 1995 he has been at the University of Edinburgh in what now is the School of Informatics. He first was a post-doc with Prof Rod Burstall, looking at applications of theorem provers to such topics as concurrent garbage-collection algorithm verification. He then in 1998 was appointed as a Lecturer and in 2011 a Senior Lecturer. From 1999 to 2011 he was also affiliated with the Institute for Systems Level Integration where he taught courses on system-on-chip design and integrated-circuit verification techniques.