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

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 cyber-physical 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 state-space 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.

• Formal verification of cache coherence protocols supporting weak memory models. To date, this has been using a model-checking approach, but I am interested too in approaches using theorem provers.
• Proof procedures for non-linear 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.

Funding

• Co-I on UKRI Grant Trustworthy Autonomous Systems Node in Governance and Regulation (EP/V026607/1). S Ramamoorthy (PI). This TAS Governance and Regulation Node is part of UKRI's Trustworthy Autonomous Systems Programme which comprises also a Hub project and 5 other Node projects. Nov 2020 -- Apr 2024.
• Microsoft Research PhD Studentship on SMT for nonlinear constraints with application to computational biology and later Validated compositional verification of ODE systems using Taylor Models. This funded the PhD of Kristjan Liiva. Jul 2014 -- Jun 2017
• Co-I on EPSRC Grant C3: Scalable & Verified Shared Memory via Consistency-directed Cache Coherence (EP/M027317/1). V. Nagarajan (PI). Nov 2015 -- Nov 2018.
• Co-I on EPSRC Platform Grant The Integration and Interaction of Multiple Mathematical Reasoning Processes (EP/N014578/1). A. Ireland (PI). Nov 2015 -- Oct 2019.
• Co-I on EPSRC Platform Grant The Integration and Interaction of Multiple Mathematical Reasoning Processes (EP/J001058/1). A. Ireland (PI).Aug 2011 -- Oct 2015.
• PI for EPSRC Grant Automatic Proof Procedures for Polynomials and Special Functions (AutoPolyFun) Nov 2010 -- Feb 2015.

Tools

• Victor, a verification condition translator for SPARK/Ada programs.

Postgraduate Students

• Ramon Fernández Mir. He developed a framework in the Lean theorem prover for the verified transformation of convex optimisation problems into forms accepted by convex optimisation tools. He completed his PhD in July 2024 and now is a formal hardware verification engineer with Apple.
• Kristjan Liiva. He investigated using compositional techniques to improve the scalability of the validated integration of ODEs arising from biological applications. He was co-supervised 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 post-docs with Taylor Johnson at Vanderbilt University, and André Platzer at Carnegie Mellon University, was a Lecturer at the University of Southampton, then Senior Research Fellow at Lancaster University on the UKRI Trustworthy Autonomous Systems Node in Security, and now is a Lecturer at Lancaster University in their School of Computing and Communications.
• Grant Olney Passmore. His PhD focussed on proof procedures for non-linear arithmetic over the rationals and reals. He graduated in summer 2011. After a post-doc with me and Lawrence Paulson on the EPSRC-funded AutoPolyFun project, he co-founded 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 HOL-light 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.
• 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

• Formal Verification, a 4th year undergraduate and MSc level course.

• 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 MSc-level course at the 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

• Tackling International Mathematical Olympiad problems and the Jordan-Hölder theorem in the Lean theorem prover.
• Verifying a security protocol in the Lean theorem prover using games, monads and probability mass functions.
• Optimising Taylor-model-based 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 SPARK-Ada programs.
• Verifying SPARK-Ada programs using a SAT modulo theories solver.
• Formalising zero-knowledge 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.

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

• a predicate subtyping extension for Isabelle/HOL,
• bus protocol specification and verification using PSL,

Administration

Biography

Aug 23-present:

Director of the AIAI Research Institute in the School of Informatics.

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 University of Cambridge, England. Electrical Sciences Tripos in 3rd year.