Paul Jackson's Home Page
I am a Senior Lecturer in the
School of Informatics
at the University of Edinburgh.
- pbj (@) inf.ed.ac.uk
10 Crichton Street
Edinburgh EH8 9AB
- [+44] (0)131 650 5131
- [+44] (0)131 651 1426
My research interests concern the development of formal
verification tools and their application in such areas as hardware
verification, software verification and formalised mathematics.
Specific current interests include:
In the past I have been interested in topics such as
- Proof procedures for non-linear arithmetic. Their
application to the formal verification of hybrid systems.
This is the topic of a newly-funded EPSRC project.
- 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
- 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
Publications, Reports and Talks
- Victor, a
verification condition translator for SPARK/Ada programs.
- RAHD, decision procedure for quantifier-free non-linear real arithmetic, written by Grant Olney Passmore
Current PhD student:
Previous PhD students include
- Andrew Sogokon. His interests are in improving
the automation of formal proofs of correctness of hybrid systems.
He started in July 2011.
Olney Passmore. His PhD focussed on proof
procedures for non-linear arithmetic over the rationals and reals
- see his home
page for details. He graduated in summer 2011. He is currently employed as a post-doc with me
on the EPSRC-funded
AutoPolyFun project which extends his research.
- 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.
Ridge. He verified a tree multicast protocol in the Isabelle
and HOL-light theorem provers, improved theorem prover automation, and
improved support for notions of proof context.
He graduated November 2006.
- Co-program chair for CAV 2010,
International conference on Computer-Aided
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
- Trustee of international CALCULEMUS Interest Group for
integrating computer algebra systems and deduction systems. Dec
09 - Nov 12.
Within the School of Informatics, I am a member of several research
for Foundations of Computer Science (LFCS), the Institute
for Computing Systems Architecture (ICSA), and
the Centre for
Intelligent Systems and their Applications.
Within CISA, I am most active
Mathematical Reasoning Group
I currently teach:
In the past I have taught such courses as
- Verification and Test I, an MSc-level course at the
System-Level Integration (ISLI). Taught
foundations of verification methodology, using Verilog as the
- Verification and Test II, an MSc-level course at the
ISLI. Taught advanced verification methodology, using
SystemVerilog as the course language.
CS/SE Individual Practical, a 3rd year
This course involved students developing a searchable
peer-to-peer database in Java.
- IP Block Integration, an
MSc module at the
This module explained how to assemble a system-level IC
design from predefined and precharacterised hardware IP
(Intellectual Property) blocks. It also covered current
techniques for hardware design verification and
design-for-test 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 data-structures.
Each year I supervise final year projects within Informatics and MSc
projects at the ISLI. Recent subjects of projects at Edinburgh
and at the ISLI:
- Verifying Spark-Ada programs using a SAT modulo theories
- Formalising zero-knowledge proofs in Isabelle.
- Evaluation of ESC/Java static assertion checker for Java.
- Hardware verification using the Cadence SMV model checker.
- A parser for the Mizar Mathematical Library.
I have also proposed project on such topics as
- Verification of a memory controller using Verisity's Specman tool
and `e' language.
- Evaluation of Specman and the `e' language using a JTAG controller
- 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.
which have not yet attracted takers. If you are at Edinburgh or the
ISLI and looking for a project topic similar to any of the above,
please get in touch.
- Building a MathWeb server for the Mizar Mathematical Library.
- A predicate subtyping extension for Isabelle/HOL.
- Bus protocol specification and verification using PSL
- Sep 11-present:
- Senior Lecturer in Informatics at University of Edinburgh
- Jan-Mar 03:
- Visiting Fellow with the
Computer Science Laboratory SRI International,
Menlo Pk, California.
- Apr 99-Aug 11:
- Lecturer in Informatics at University of Edinburgh and in
System Level Integration at Institute for System level Integration
- 98-Mar 99
- Lecturer in Informatics at University of Edinburgh.
- Research Fellow in Computer Science at University of
- MS, PhD degrees and post-doc in Computer Science at
Cornell University, Ithaca NY, USA. Most of this time I was
involved with the
- MS in Physics at Cornell University.
Studied electron spin resonance in sapphire substrates using
superconducting microstrip resonators.
- Designed application-specific ICs for US General Electric in
North Carolina, USA.
- Undergraduate in Engineering at Cambridge, England. Electrical
Sciences Tripos in 3rd year.
Last modified: Wed 30 May 2012