Paul Jackson's Home Page
I am a Senior Lecturer in the
School of Informatics at
the University of Edinburgh and
Director of the AIAI
research institute. The AIAI (the Artificial Intelligence
and its Applications Institute) is one of
the six
research institutes in the School.

 email:
 Paul.Jackson (@) ed.ac.uk
 address:

Room 2.12
Informatics Forum
10 Crichton Street
Edinburgh EH8 9AB
United Kingdom
 phone:
 [+44] (0)131 650 5131
 fax:
 [+44] (0)131 651 1426

Research
Interests
My research interests concern the development of
formal verification
tools and their application in such areas as hardware verification, software verification,
robotics, systems biology and formalised mathematics.
Specific current interests include:
 Use of the Lean theorem prover for the verified translation
of convex optimisation problems into forms in which they can be
solved by convex optimisation tools.
 Formal verification of hybrid systems,
popular models of cyberphysical systems such as robots and autonomous vehicles.
Hybrid systems describe continuous behaviour using differential equations
and specify conditions for switching between different modes of behaviour. I am interested in
 deductive techniques using theorem provers such as
KeYmaera,
Isabelle and Lean,
 automated statespace exploration techniques such as used by the Flow* tool,
and the combination of both these kinds of techniques.
 Approaches for dynamically presenting formal proofs
developed using interactive theorem provers.
In the past, topics I have been interested in include:
 Formal verification of cache coherence protocols supporting weak memory models.
To date, this has been using a modelchecking approach,
but I am interested too in approaches using theorem provers.
 Proof procedures for nonlinear arithmetic and their
application to hybrid systems verification.
 Using SMT solvers and interactive theorem provers to prove
software verification conditions. I have developed a tool, Victor, for augmenting the
capabilities of the tools available for formally analysing
programs written in the SPARK subset of
Ada.
 Space efficient and high performance encodings of linear
temporal logic bounded model checking problems into SAT
(propositional satisfiability) problems.
 Combining model checking and mechanical theorem proving techniques
in order to verify hardware. Generalising abstraction methods.
 Importing formal developments of mathematics in the Mizar mathematical language
into other theorem provers such as Isabelle.
 The design and use of interactive theorem provers. I undertook
extensive work on
Nuprl for my PhD and have experience with using
PVS.
If you are looking to do a PhD and any of the above subject areas
interest you, please get in touch; I would be happy to discuss
possible PhD topics with you.
Publications, Reports and Talks
(click to view)
Funding
Current:
Recent:
Tools
 Victor, a
verification condition translator for SPARK/Ada programs.
Postgraduate Students
Current PhD student:
 Ramon
Fernández Mir. He started in September 2020 and
expects to submit his PhD thesis in spring 2024. His thesis is on
a developing a framework in the Lean theorem prover for the
verified transformation of convex optimisation problems into forms
accepted by convex optimisation tools.
Previous PhD students include
 Kristjan Liiva. He investigated using
compositional techniques to improve the scalability of the
validated integration of ODEs arising from biological
applications. He was cosupervised by
Grant Passmore at Aesthetic
Integration
and Christoph Wintersteiger, then at Microsoft Research, Cambridge. He
successfully defended his PhD thesis in January 2019.
 Andrew Sogokon. His interests were in improving
the automation of formal proofs of correctness of hybrid systems.
He completed his PhD January 2016, had postdocs with
Taylor Johnson at Vanderbilt University,
and
André
Platzer at Carnegie Mellon University, was
a Lecturer at the University of Southampton. Currently he is a
Senior Research Fellow at Lancaster University on the UKRI
Trustworthy Autonomous Systems Node in Security.
 Grant
Olney Passmore. His PhD focussed on proof
procedures for nonlinear arithmetic over the rationals and reals.
He graduated in summer 2011. After a postdoc with me and Lawrence Paulson
on the EPSRCfunded
AutoPolyFun project, he cofounded
in 2014 the financial technology startup Aesthetic Integration, now rebranded as Imandra.
 Daniel Sheridan. He looked at novel encodings of bounded model
checking problems into propositional satisfiability problems which
can be checked by SAT solvers. He graduated November 2006, worked for the formal methods
consultancy Adelard until 2015, and now works for Google.
 Tom Ridge. He
verified a tree multicast protocol in the Isabelle and
HOLlight theorem provers, improved theorem prover automation,
and improved support for notions of proof context. He
graduated November 2006, was then a Lecturer and subsequently a
Senior Lecturer in the Department of Computer Science at the
University of Leicester until 2021, and is now a software
engineer.
Professional Activities
 Program Committee for CICM 2017, the 10th Conference on Intelligent Computer Mathematics, Calculemus track.
 Program Committee for CADE 2013, the 24th International Conference on Automated Deduction.
 Coprogram chair for CAV 2010,
International conference on ComputerAided
Verification. July 2010
 Program Committee for VERIFY 2010, 6th International Verification Workshop.
 Program Committee for AFM 2010, 5th
Workshop on Automated Formal Methods
 Program Committee for WING 2009, Workshop on
Invariant Generation
 Trustee of international CALCULEMUS Interest Group for
integrating computer algebra systems and deduction systems. Dec
09  Nov 12.
Local Affiliations
Within the School of Informatics, I am a member of
the Artificial
Intelligence and its Applications Institute (AIAI) and
the Laboratory
for Foundations of Computer Science (LFCS),
and an associate member of the Institute
for Computing Systems Architecture (ICSA).
Teaching
Courses
In the 202324 academic year I am teaching
In the past, other courses I have taught or cotaught include:
 Informatics Large Practical, a 3rd year undergraduate course.
 Introduction to Software Engineering, a 2nd year undergraduate course.
 Automated Reasoning, a 4th year undergraduate and MSc level course that covered
interactive theorem proving and model checking.
 Introduction to Computer Systems, a 2nd year undergraduate course.
 Verification and Test I, an MSclevel course at the ISLI.
Taught foundations of verification methodology, using Verilog as the
course language.
 Verification and Test II, an MSclevel course at the
ISLI. Taught advanced verification methodology, using
SystemVerilog as the course language.
 The CS/SE Individual Practical, a 3rd year
undergraduate course.
This course involved students developing a searchable
peertopeer database in Java.
 IP Block Integration, an
MSc module at the
ISLI.
This module explained how to assemble a systemlevel IC
design from predefined and precharacterised hardware IP
(Intellectual Property) blocks. It also covered current
techniques for hardware design verification and
designfortest approaches. The main practical work centered around
the e hardware verification language.
 Computer Science 1, a 1st year undergraduate course
in the School of Informatics.
This course was taken by all students on Informatics related
degrees. It covered topics such as programming in Java,
software engineering, and algorithms and datastructures.
The ISLI was the Institute for SystemLevel Integration,
a venture run between 1999 and 2011 by 4 Scottish universities,
including the University of Edinburgh, for the promotion of
systemonchip integrated circuit design.
Projects
Each year I supervise finalyear undergraduate and MSc projects.
Recent subjects of projects at Edinburgh include:
 Tackling International Mathematical Olympiad problems and the
JordanHölder theorem in the Lean theorem prover.
 Verifying a security protocol in the Lean theorem prover
using games, monads and probability mass functions.
 Optimising Taylormodelbased validated integration.
 Formalising the metatheory of session types in the Lean theorem prover.
 Developing a theory of multivariate polynomials in the Lean theorem prover.
 Verifying software using Dafny.
 Using Boogie to verify SPARKAda programs.
 Verifying SPARKAda programs using a SAT modulo theories
solver.
 Formalising zeroknowledge proofs in Isabelle.
 Evaluation of the ESC/Java static assertion checker for Java.
 Hardware verification using the Cadence SMV model checker.
 A parser for the Mizar Mathematical Library.
Up till 2011 I supervised MSc projects at the Institute for System Level Integration.
Projects included:
 Verification of a memory controller using Verisity's Specman tool
and `e' language.
 Evaluation of Specman and the `e' language using a JTAG controller
case study.
 Overcoming the Challenges of Timing Convergence for Next
Generation SoC ASIC Devices.
 Formal Verification of a RTL IP Block using Cadence FormalCheck.
 Analysis of Serial RapidIO performance and implementation of
part of the physical layer specification.
I have also proposed project on such topics as
 a predicate subtyping extension for Isabelle/HOL,
 bus protocol specification and verification using PSL,
which have not yet attracted takers. If you are
looking for a project topic similar to any of the above,
please get in touch.
Administration
Currently I am Director of
the AIAI research
institute in the School of Informatics. In the past my
mostmajor adminstrative roles in the School have been that
of Senior Tutor (201822, 201214) and, before that, the
similar Senior Director of Studies (200912). These
roles involved providing support and advice to the School's
Personal Tutors and Directors of Studies, and figuring out ways
forward for students who were having difficulty with their studies.
Biography
 Aug 23present:
 Director of the
AIAI Research
Institute in the School of Informatics.
 Sep 11present:
 Senior Lecturer in Informatics at University of Edinburgh
 JanMar 03:
 Visiting Fellow with the
Computer Science Laboratory SRI International,
Menlo Pk, California.
 Apr 99Aug 11:
 Lecturer in Informatics at University of Edinburgh and in
System Level Integration at Institute for System level Integration
 98Mar 99
 Lecturer in Informatics at University of Edinburgh.
 9598
 Research Fellow in Computer Science at University of
Edinburgh.
 8895:
 MS, PhD degrees and postdoc in Computer Science at
Cornell University, Ithaca NY, USA. Most of this time I was
involved with the
Nuprl project.
 8688:
 MS in Physics at Cornell University.
Studied electron spin resonance in sapphire substrates using
superconducting microstrip resonators.
 8486:
 Designed applicationspecific ICs for US General Electric in
North Carolina, USA.
 8184:
 Undergraduate in Engineering at University of Cambridge, England. Electrical
Sciences Tripos in 3rd year.
Paul Jackson
Last modified: Wed 1 Nov 2023