Paul Jackson: Publications, Reports and Talks

Refereed Conference and Workshop Publications

• 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. abstract , dvi(23K), ps(147K). © 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. abstract , dvi(30K), ps(92K). © 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. abstract , dvi(40K), ps(106K).
• 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. 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 A-10. North-Holland, 1992. abstract , dvi(39K), ps(76K).
• 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.

Reports

• 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

• Paul B. Jackson, Grant Olney Passmore. Proving SPARK Verification Conditions with SMT solvers. December 2009. pdf
• Paul B. Jackson. Formalization of Divisibility Theory in Nuprl. January 1997. abstract , dvi(49K), ps(125K).

  An automatically-generated hypertext presentation of the Nuprl theory this paper is based on can be viewed by following this link.

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. 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

• 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

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. The listings for the polynomial-related theories are not included at the moment, but might be in the future.