Paul Jackson's Home Page

I am a Senior Lecturer in the School of Informatics at the University of Edinburgh.

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

fax:

[+44] (0)131 651 1426

Research

Interests

Specific current interests include:

• 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 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.

Funding

• PI for EPSRC Grant Automatic Proof Procedures for Polynomials and Special Functions (AutoPolyFun) Nov 2010 -- Oct 2014.
• One of UK representatives for EU COST Action IC0901 Rich Model Toolkit - An Infrastructure for Reliable Computer Systems
• Co-I on EPSRC Platform Grant The Integration and Interaction of Multiple Mathematical Reasoning Processes (EP/J001058). A. Ireland (PI).Aug 2011 -- Jul 2015.

Tools

• Victor, a verification condition translator for SPARK/Ada programs.
• RAHD, decision procedure for quantifier-free non-linear real arithmetic, written by Grant Olney Passmore

Postgraduate Students

• Andrew Sogokon.
His interests are in improving the automation of formal proofs of correctness of hybrid systems. He started in July 2011.

• Grant 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.
• 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.

Professional Activities

• 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 Invariant Generation
• Trustee of international CALCULEMUS Interest Group for integrating computer algebra systems and deduction systems. Dec 09 - Nov 12.

Local Affiliations

Teaching

Courses

• Automated Reasoning, a 4th year undergraduate and MSc level course.
• Introduction to Computer Systems, a 2nd year undergraduate course.

• Verification and Test I, an MSc-level course at the Institute for System-Level Integration (ISLI). Taught foundations of verification methodology, using Verilog as the course language.
• Verification and Test II, an MSc-level 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 peer-to-peer database in Java.
• IP Block Integration, an MSc module at the ISLI. 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.

Projects

• 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.

• 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.

• Building a MathWeb server for the Mizar Mathematical Library.
• A predicate subtyping extension for Isabelle/HOL.
• Bus protocol specification and verification using PSL

Biography

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.

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.