About Me
Welcome! I'm Jamie Wright, a Research Associate and PhD candidate in the Security Of Advanced Systems/Foundations Of Logic group at the University of Sheffield.
My primary research interests are formal methods for security and proof-theoretic approaches, particularly in Isabelle/HOL under the supervision of Dr. Andrei Popescu.
I'm currently working on the COVERT project (alongside collaborators in Kent/Surrey), which aims to provide reusable models, tools and techniques that enable the verification of safety and security properties over a range of advanced architectures.
Alongside this work, I am collaborating with Liron Cohen and Reuben Rowe on formalising Infinite Descent, with long-term plans to develop an object logic/Sledgehammer-like tool for Isabelle that integrates this soundness principle.
I'm grateful to have my studies fully funded by the EPSRC Doctoral Training Partnership (DTP).
Previously, I completed my BSc(Hons I) in Computer Science and Mathematics w/ Year in Industry at the University Of Sheffield. My dissertation involved abstracting a generic two-player game and characterising a general winning strategy - formalised in Isabelle/HOL - with potential for instantiation in games such as Chess. have also worked alongside Dr. James Cranch on utilising the SAGE Maths extension of Python to solve Olympiad maths questions in the context of Euclidean Geometry, under the SURE research scheme.
Beyond my research, I am also a passionate teacher, with over 5 years of formal experience, delivering seminars up to a Master's level in Computer Science, and undergraduate in Mathematics. My teaching interests (in part) cover Logic, Programming Languages, Algebra and Piano.
Outside of work, I am a passionate musician, having achieved Grade 5 in both music theory and practical piano, alongside being an avid climber.
Selected Publication
Certified Infinite Descent Criteria in Isabelle/HOL
17th International Conference on Interactive Theorem Proving
Infinite Descent is the global trace condition that underpins the soundness of cyclic reasoning and, in program analysis, the size change termination principle. Many (semi-)decision procedures for Infinite Descent are known, based on criteria ranging from automata-based constructions and relation-based characterizations, to effective (but incomplete) heuristics. Although these criteria are well studied on paper and implemented in tools, a unified, machine-checked account that relates them to the (abstract) Infinite Descent property has been missing. We present an Isabelle/HOL mechanization of this landscape. We develop a reusable, locale-based framework of sloped graphs that defines Infinite Descent at an abstract level, independently of any concrete graph encoding. Within this framework we formalize standard complete criteria and prove their equivalence to the locale-level InfiniteDescent predicate. We also formalize tool-facing sufficient criteria, prove their soundness, and certify incompleteness where appropriate via verified counterexamples. Along the way we contribute reusable Isabelle lemmas for omega-regular reasoning over streams and for Buchi-automata constructions needed by the inclusion proofs.
Read more
