Paul Jackson: Publications, Reports and Talks
Refereed Conference and Workshop Publications

Paul Jackson,
Andrew Sogokon,
James Bridge and
Lawrence Paulson.
Verifying Hybrid Systems Involving Transcendental Functions
.
6th NASA Formal Methods Symposium. April 2014.
Lecture Notes in Computer Science. Vol 8430. pp188202. Springer.
pdf.
© SpringerVerlag.

Paul Jackson, Florian Schanda and Angela Wallenburg.
Auditing UserProvided Axioms in Software Verification
Conditions. Formal Methods for Industrial Critical Systems
18th International Workshop
(FMICS). September 2013. Lecture Notes
in Computer Science, Vol. 8187. pp 154168. Springer.
pdf.
© SpringerVerlag.

Grant Olney Passmore and Paul B. Jackson.
Abstract
Partial Cylindrical Algebraic Decomposition I: The Lifting Phase
Computability in Europe (CiE) 2012: Turing Centenary Conference.
Lecture Notes in Computer Science, Vol. 7318. Springer.

Grant Olney Passmore, Leonardo de Moura and Paul B. Jackson.
Gröbner Basis Construction Algorithms Based on Theorem
Proving Saturation Loops. Decision Procedures in Software,
Hardware and Bioware. Dagstuhl Seminar Proceedings,
No. 10161. 2010.

Grant Olney Passmore and Paul B. Jackson.
Combined Decision Techniques for the Existential Theory
of the Reals.
16th Symposium on the Integration of
Symbolic Computation and Mechanised Reasoning,
Calculemus
2009, Grand Bend, Ontario, Canada, July 2009.
pdf.
© SpringerVerlag.
 Paul B. Jackson, Bill J. Ellis and Kathleen Sharp.
Using SMT Solvers to Verify HighIntegrity Programs.
2nd International Workshop on Automated Formal Methods,
AFM '07,
Atlanta, Georgia, USA,
6th November 2007.
pdf
© ACM.
 Paul B. Jackson and Daniel Sheridan.
A Compact Linear Translation for Bounded
Model Checking. 4th International Workshop
on Bounded Model Checking,
BMC'06.
Seattle, August 15, 2006.
Revised version in Vol 174, Issue 3, Pages 1730,
Electronic Notes in Theoretical Computer Science, May 2007.
paper (pdf)
© Elsevier,
slides (pdf).
 Paul B. Jackson. Nuprl . Ch 14 of
Freek Wiedijk (ed.),"The Seventeen Provers of the World",
foreword by Dana Scott. pp116126, Vol 3600,
Lecture Notes in Computer Science ,
SpringerVerlag, Jan 2006.
pdf
© SpringerVerlag.
 Paul Jackson and Daniel Sheridan.
Clause Form Conversions for Boolean Circuits.
In SAT 2004
(7th International Conference on Theory and
Applications of Satisfiability Testing), selected revised
papers. pp183198, Vol 3542,
Lecture Notes in Computer Science ,
SpringerVerlag, Aug 2005.
pdf
© SpringerVerlag.
 Graeme Cunningham, Paul B. Jackson and Julian A. B. Dines.
Expression Coverability Analysis: Improving Code Coverage
Analysis with Model Checking.
Design and Verification Conference (DVCon), San Jose, March 2004.
pdf
 Paul B. Jackson.
Total Correctness Refinement for Sequential Reactive
Systems.
In proceedings of TPHOLs 2000. (13th
International Conference on Theorem Proving in Higher Order
Logics), August 2000. pp320337, Vol. 1869,
Lecture Notes in Computer Science ,
SpringerVerlag.
pdf.
© SpringerVerlag.
 Paul B. Jackson.
Verifying a Garbage Collection Algorithm.
In Proceedings of TPHOLs'98 (11th
International Conference on Theorem Proving in Higher Order
Logics), September 1998.
pp225244, Vol. 1479,
Lecture Notes in Computer Science ,
SpringerVerlag.
pdf.
© SpringerVerlag.
 Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan
Uribe. Constructively Formalizing Automata Theory
. In Proof, Language and
Interaction: Essays in Honour of Robin Milner
. Eds. Gordon Plotkin, Colin Stirling, Mads
Tofte. MIT Press, 2000.
pdf.
 Paul B. Jackson. Exploring Abstract Algebra in
Constructive Type Theory. In A. Bundy, editor,
12th International Conference on
Automated Deduction, Lecture Notes in Artifical
Intelligence. SpringerVerlag, June 1994.
abstract ,
dvi(25K),
ps(59K).
 Paul B. Jackson.
Nuprl and its Use in Circuit Design. In
R.T. Boute, V. Stavridou, T.F.Melham,editors, Proceedings of
the 1992 Interational Conference on Theorem Provers in Circuit
Design, IFIP Transactions A10. NorthHolland, 1992.
abstract ,
dvi(39K),
ps(76K).
 Paul B. Jackson.
Developing a Toolkit for FloatingPoint Hardware in
the Nuprl Proof Development System. In Proceedings
of the Advanced Research Workshop on correct Hardware Design
Methodologies. Elsevier, 1991.
Notes and Reports

Kristjan Liiva,
Grant Passmore and
Paul Jackson.
A note on real quantifier elimination by virtual term substitution of unbounded
degree. Presented at PAS 2014, the
Third International Seminar on Program Verification, Automated Debugging and Symbolic Computation.
Vienna, Austria. July 2014.
pdf.
 Paul Jackson and Daniel Sheridan,
The Optimality of a Fast CNF Conversion and its Use with SAT
APES Report APES822004, March 2004.
ps
Draft Papers
Talks
 Paul B. Jackson.
Expressive Typing and Abstract Theories in Nuprl and PVS.
Slides from invited tutorial given at TPHOLs (International
Conference on Theorem Proving in
HigherOrder Logics) '96 in Turku, Finland, August 1996.
abstract ,
dvi(13K),
ps(92K).
 Paul B. Jackson.
Can we Resolve the Tension between Constructive
Type Theorists and Classical Mathematicians?
Summary of talk given at the Second QED workshop in Warsaw, Poland,
July 1995.
dvi (7K),
ps (23K).
Edited Conference Proceedings
 Tayssir Touili, Byron Cook and Paul Jackson Eds., Proceedings of the 22nd International Conference on Computer Aided Verification, CAV 2010.
Vol 6174, Lecture Notes in Computer Science, Springer, July 2010.
 Richard J. Boulton and Paul B. Jackson Eds., Proceedings of
14th International Conference on Theorem Proving in Higher
Order Logics (TPHOLs) 2001.
Vol 2152, Lecture Notes in Computer Science, Springer, Sept. 2001.
Manuals
 Paul B. Jackson.
The Nuprl Proof Development System, Version 4.2.
Reference Manual and User's Guide. July 29th 1995.
ps (300K).
PhD Thesis
My PhD thesis entitled Enhancing the Nuprl Proof Development
System and Applying it to Computational Abstract Algebra is
available.
abstract ,
dvi,
ps.
pdf.
It has also been issued as Cornell University Computer Science
Technical Report TR951509 which is available from the Cornell University Library Technical Reports and Papers archive.
Hypertext listings for most of the
theories I developed for my thesis are available. The listings for
each theory include introductions, summaries of definitions and
theorems, and formatted proofs. Hypertext listings for the
polynomialrelated theories are not currently available, but plain PDF listings are:
 polynom_1

Class definitions for free abelian monoid, monoid copower,
free monoid algebra and polynomial algebra.
Without proofs.
With proofs.
 polynom_2
 Implementation of free abelian monoid using alists.
Without proofs.
With proofs.
 polynom_3
 Implementation of free monoid algebra using alists.
Without proofs.
With proofs.
 polynom_4

Combination of implementations from polynom_2 and polynom_3
to form polynomial algebra.
Without proofs.
With proofs.
Paul Jackson
Last modified: Wed 5 Nov 2014