Paul Jackson's Home Page
I am a lecturer both in the
School of Informatics
at the University of Edinburgh
and at the Institute for
System Level Integration (ISLI) in Livingston, Scotland.
- email:
- pbj (@) inf.ed.ac.uk
- address:
-
Room 4.05
Informatics Forum
10 Crichton Street
Edinburgh EH8 9AB
United Kingdom
- phone:
- [+44] (0)131 650 5131
Research
Interests
My research interests concern the development and application of
formal verification tools. In the past I mostly worked with
mechanical theorem proving tools such as
Nuprl and PVS. More
recently I have also been interested in bounded and unbounded
model checking and SMT (SAT modulo theory) solvers. Application
areas I have been interested in include hardware verification,
software verification and formalised mathematics.
Specific current interests include:
- Using SMT solvers and other automated reasoning techniques
to prove software verification conditions. One focus is on
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.
Publications, Reports and Talks
Postgraduate Students
Current PhD student:
- Grant
Olney Passmore. His current interests include proof
procedures for non-linear arithmetic over the rationals and reals -
see his home
page for details. He started autumn 2007.
Previous PhD students include
- 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.
- Tom
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.
Affiliations
Within the School of Informatics, I am a member of several research
institutes:
the Laboratory
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
with the
Mathematical Reasoning Group
Teaching
Courses
My teaching for the 08-09 academic session includes:
- The
CS/SE Individual Practical, a 3rd year undergraduate
course in the School of Informatics.
This course involves students developing a searchable
peer-to-peer database in Java.
- IP Block Integration, an
MSc module at the ISLI.
This module explains how to assemble a system-level IC design
from predefined and precharacterised hardware IP (Intellectual
Property) blocks.
It also covers current techniques for hardware design verification
and design-for-test approaches.
In the recent past I have also taught:
- 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.
Projects
Each year I supervise final year projects within Informatics and MSc
projects at the ISLI. Recent subjects of projects at Edinburgh
include:
- Verifying Spark-Ada programs using a SAT modulo theories
solver.
- 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.
and at the ISLI:
- 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
- Building a MathWeb server for the Mizar Mathematical Library.
- A predicate subtyping extension for Isabelle/HOL.
- Bus protocol specification and verification using PSL
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.
Biography
- Jan-Mar 03:
- Visiting Fellow with the
Computer Science Laboratory SRI International,
Menlo Pk, California.
- Apr 99-present:
- Lecturer in Informatics at University of Edinburgh and in
System Level Integration at Institute for System level Integration
in Livingston, Scotland.
- 98-Mar 99
- Lecturer in Informatics at University of Edinburgh.
- 95-98
- Research Fellow in Computer Science at University of
Edinburgh.
- 88-95:
- MS, PhD degrees and post-doc in Computer Science at
Cornell University, Ithaca NY, USA. Most of this time I was
involved with the
Nuprl project.
- 86-88:
- MS in Physics at Cornell University.
Studied electron spin resonance in sapphire substrates using
superconducting microstrip resonators.
- 84-86:
- Designed application-specific ICs for US General Electric in
North Carolina, USA.
- 81-84:
- Undergraduate in Engineering at Cambridge, England. Electrical
Sciences Tripos in 3rd year.
Paul Jackson
Last modified: Fri Aug 22 10:24:14 BST 2008