Paul Jackson - Lecturer

Interests
My research interests include: the design of mechanical theorem proving environments, their use for software and hardware development and for general-purpose mathematics, and integrating theorem provers with other reasoning techniques such as model checking. I have most experience with the Nuprl and PVS theorem provers.
Specific current interests include:

Combining model checking and mechanical theorem proving techniques in order to verify hardware. Generalising abstraction methods.
Using a theorem prover to support the analysis of stochastic systems described using stochastic process algebras.
Importing formal developments of mathematics in the Mizar mathematical language into other theorem provers such as Isabelle.
See also below where I describe the topics my postgraduate students are working on.