Nuprl and Its Use in Circuit Design. - Paul B. Jackson (TPCD, 1992)

Exploring Abstract Algebra in Constructive Type Theory. - Paul B. Jackson (CADE, 1994)

Enhancing the NUPRL Proof Development System and Applying it to Computational Abstract Algebra. - Paul B. Jackson (1995)

Verifying a Garbage Collection Algorithm. - Paul B. Jackson (TPHOLs, 1998)

Constructively formalizing automata theory. - Robert L. Constable; Paul B. Jackson; Pavel Naumov; Juan C. Uribe (Proof, Language, and Interaction, 2000)

Total-Correctness Refinement for Sequential Reactive Systems. - Paul B. Jackson (TPHOLs, 2000)

Clause Form Conversions for Boolean Circuits. - Paul B. Jackson; Daniel Sheridan (SAT (Selected Papers, 2004)

Nuprl. - Paul B. Jackson (The Seventeen Provers of the World, 2006)

A Compact Linear Translation for Bounded Model Checking. - Paul B. Jackson; Daniel Sheridan (BMC@FLoC, 2006)

Combined Decision Techniques for the Existential Theory of the Reals. - Grant Olney Passmore; Paul B. Jackson (Calculemus/MKM, 2009)

Gröbner Basis Construction Algorithms Based on Theorem Proving Saturation Loops. - Grant Olney Passmore; Leonardo Mendonça de Moura; Paul B. Jackson (Decision Procedures in Software, Hardware and Bioware, 2010)

Abstract Partial Cylindrical Algebraic Decomposition I: The Lifting Phase. - Grant Olney Passmore; Paul B. Jackson (CiE, 2012)

Auditing User-Provided Axioms in Software Verification Conditions. - Paul B. Jackson; Florian Schanda; Angela Wallenburg (FMICS, 2013)

Verifying Hybrid Systems Involving Transcendental Functions. - Paul B. Jackson; Andrew Sogokon; James P. Bridge; Lawrence C. Paulson (NASA Formal Methods, 2014)

Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems. - Andrew Sogokon; Paul B. Jackson (FM, 2015)

A Method for Invariant Generation for Polynomial Continuous Systems. - Andrew Sogokon; Khalil Ghorbal; Paul B. Jackson; André Platzer (VMCAI, 2016)

Verification of a lazy cache coherence protocol against a weak memory model. - Christopher J. Banks; Marco Elver; Ruth Hoffmann; Susmit Sarkar; Paul B. Jackson; Vijay Nagarajan (FMCAD, 2017)

Verifying Safety and Persistence Properties of Hybrid Systems Using Flowpipes and Continuous Invariants. - Andrew Sogokon; Paul B. Jackson; Taylor T. Johnson (NFM, 2017)

VerC3: A library for explicit state synthesis of concurrent systems. - Marco Elver; Christopher J. Banks; Paul B. Jackson; Vijay Nagarajan (DATE, 2018)

Compositional Taylor Model Based Validated Integration. - Kristjan Liiva; Paul B. Jackson; Grant O. Passmore; Christoph M. Wintersteiger (SYNASC, 2018)

Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants. - Andrew Sogokon; Paul B. Jackson; Taylor T. Johnson (J. Autom. Reason., 2019)

Transforming Optimization Problems into Disciplined Convex Programming Form. - Ramon Fernández Mir; Paul B. Jackson; Siddharth Bhat; Andrés Goens; Tobias Grosser (CICM, 2024)