Paul Jackson: Publications, Reports and Talks
Most of the publications below can also be found referenced on my
DBLP and
Google
Scholar pages.
Journal Publications
- Andrew Sogokon, Paul B. Jackson, Taylor T. Johnson.
Verifying safety and persistence in hybrid systems using
flowpipes and continuous invariants.
Journal of Automated Reasoning.
Published online 24 November 2018. © Springer Nature B.V.
Refereed Conference and Workshop Papers, Book Chapters
- Ramon Fernández Mir, Paul B. Jackson, Siddharth Bhat, Andrés Goens, Tobias Grosser.
Transforming Optimization Problems into Disciplined Convex Programming Form.
CICM 24: Intelligent Computer Mathematics, 17th International Conference. pp183-202. Jul 2024 (online).
Springer, Cham.
Accepted manuscript,
Publisher's page.
- Paul B. Jackson.
Dynamic Proof Presentation. Ch 4 of G. Michaelson (ed.),
"Mathematical Reasoning: The History and Impact of the DReaM Group".
pp63-86. May 2021 (online). Springer, Cham.
Accepted manuscript,
Publisher's page.
-
Kristjan Liiva, Paul B. Jackson, Grant O. Passmore, Christoph M. Wintersteiger.
Compositional Taylor Model Based Validated Integration.
SYNASC 18: Symbolic and Numeric Algorithms for Scientific Computing,
20th International Symposium.
Sep 2018.
Accepted manuscript,
Publisher's page.
-
Marco Elver, Christopher J. Banks, Paul Jackson, Vijay Nagarajan.
VerC3: A Library for Explicit State Synthesis of Concurrent
Systems. DATE 18: Design and Test Europe.
To appear in ACM and IEEE Digital Libraries, Mar 2018.
pdf.
-
Christopher J. Banks, Marco Elver, Ruth Hoffmann, Susmit Sarkar,
Paul Jackson, Vijay Nagarajan.
Verification of a lazy cache coherence protocol
against a weak memory model.
FMCAD 17: Formal Methods for Computer-Aided Design.
To appear in ACM and IEEE Digital Libraries, Oct 2017.
pdf.
- Andrew Sogokon, Paul B. Jackson, Taylor T. Johnson.
Verifying safety and persistence properties of hybrid
systems using flowpipes and continuous invariants.
NFM 17: NASA Formal Methods, 9th Symposium.
Lecture Notes in Computer Science. Springer.
pdf.
© Springer-Verlag.
- Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson, and Andre Platzer.
A Method for Invariant Generation for Polynomial Continuous Systems. VMCAI 2016: Verification, Model Checking and Abstract Interpretation, 17th International Conference.
Lecture Notes in Computer Science. Vol 9583, pp. 268-288. Springer
pdf.
© Springer-Verlag.
-
Andrew Sogokon and
Paul B. Jackson.
Direct formal verification of liveness properties in continuous and
hybrid dynamical systems.
FM 2015:
Formal Methods, 20th International Symposium.
June 2015.
Lecture Notes in Computer Science. Vol 9109. pp514-531. Springer.
pdf.
© Springer-Verlag.
-
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. pp188-202. Springer.
pdf.
© Springer-Verlag.
-
Paul Jackson, Florian Schanda and Angela Wallenburg.
Auditing User-Provided 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 154-168. Springer.
pdf.
© Springer-Verlag.
-
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.
© Springer-Verlag.
- Paul B. Jackson, Bill J. Ellis and Kathleen Sharp.
Using SMT Solvers to Verify High-Integrity 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 17-30,
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. pp116-126, Vol 3600,
Lecture Notes in Computer Science ,
Springer-Verlag, Jan 2006.
pdf
© Springer-Verlag.
- 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. pp183-198, Vol 3542,
Lecture Notes in Computer Science ,
Springer-Verlag, Aug 2005.
pdf
© Springer-Verlag.
- 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. pp320-337, Vol. 1869,
Lecture Notes in Computer Science ,
Springer-Verlag.
pdf.
© Springer-Verlag.
- 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.
pp225-244, Vol. 1479,
Lecture Notes in Computer Science ,
Springer-Verlag.
pdf.
© Springer-Verlag.
- 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. Springer-Verlag, June 1994.
pdf.
- 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 A-10. North-Holland, 1992.
pdf.
- Paul B. Jackson.
Developing a Toolkit for Floating-Point 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 APES-82-2004, 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
Higher-Order Logics) '96 in Turku, Finland, August 1996.
pdf.
- 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.
pdf.
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.
pdf
PhD Thesis
My PhD thesis entitled Enhancing the Nuprl Proof Development
System and Applying it to Computational Abstract Algebra is
available.
pdf.
It has also been issued as Cornell University Computer Science
Technical Report TR95-1509 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
polynomial-related 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 a-lists.
Without proofs.
With proofs.
- polynom_3
- Implementation of free monoid algebra using a-lists.
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 24 Nov 2021