معرفی
Paul Jackson is a Senior Lecturer in the School of Informatics at the University of Edinburgh and serves as Director of the Artificial Intelligence and its Applications Institute (AIAI). He is also affiliated with the Laboratory for Foundations of Computer Science (LFCS) and is an associate member of the Institute for Computing Systems Architecture (ICSA). His work bridges theoretical and applied aspects of formal methods in computer science.
Education
- PhD and MS in Computer Science, Cornell University (1988–1995)
- MS in Physics, Cornell University (1986–1988)
- Undergraduate in Engineering, University of Cambridge (1981–1984)
Paul Jackson's research focuses on formal verification, particularly the development and application of tools for verifying software, hardware, and hybrid systems. His primary interests include interactive theorem proving (using Lean, Isabelle, and KeYmaera), formal verification of hybrid and cyber-physical systems, non-linear arithmetic, and the integration of symbolic computation with deduction. He has worked extensively with the Nuprl theorem prover and contributed to tools like Victor for SPARK/Ada verification.
His recent publications emphasize compositional verification, validated integration using Taylor models, invariant generation for polynomial systems, and dynamic proof presentation. He has been involved in multiple EPSRC and UKRI-funded projects, including work on trustworthy autonomous systems and cache coherence protocols.
Scientific Awards and Recognition
- No specific awards are listed in the provided text.
Paul Jackson has advised several PhD students, including Ramon Fernández Mir, Kristjan Liiva, Andrew Sogokon, and Grant Olney Passmore, many of whom have gone on to influential roles in academia and industry. He has held significant administrative roles, including Senior Tutor and Senior Director of Studies, and has contributed to major conferences such as CAV, CICM, and CADE as program committee member or chair. His teaching includes courses on formal verification, automated reasoning, and software engineering.
