| Enhancing the Nuprl proof development system and applying it to computational abstract algebra PB Jackson Cornell University, 1995 | 125 | 1995 |
| Clause form conversions for boolean circuits P Jackson, D Sheridan International Conference on Theory and Applications of Satisfiability …, 2004 | 112 | 2004 |
| The Nuprl proof development system, version 4.2 reference manual and user’s guide P Jackson Cornell University, Ithaca, NY, 1994 | 51 | 1994 |
| Combined decision techniques for the existential theory of the reals GO Passmore, PB Jackson International Conference on Intelligent Computer Mathematics, 122-137, 2009 | 50 | 2009 |
| Exploring abstract algebra in constructive type theory P Jackson Automated Deduction—CADE-12: 12th International Conference on Automated …, 1994 | 48 | 1994 |
| Verifying a garbage collection algorithm PB Jackson International Conference on Theorem Proving in Higher Order Logics, 225-244, 1998 | 44 | 1998 |
| A method for invariant generation for polynomial continuous systems A Sogokon, K Ghorbal, PB Jackson, A Platzer International Conference on Verification, Model Checking, and Abstract …, 2015 | 42 | 2015 |
| Constructively formalizing automata theory RL Constable, PB Jackson, P Naumov, J Uribe | 42 | 2000 |
| Using SMT solvers to verify high-integrity programs PB Jackson, BJ Ellis, K Sharp Proceedings of the second workshop on Automated formal methods, 60-68, 2007 | 31 | 2007 |
| Nuprl and Its Use in Circuit Design. PB Jackson TPCD, 311-336, 1992 | 19 | 1992 |
| Computer Aided Verification T Touili, B Cook, P Jackson Lecture Notes in Computer Science 6174, 2010 | 17 | 2010 |
| Formalizing automata II: Decidable properties RL Constable, PB Jackson, P Naumov, J Uribe Cornell University, 1997 | 17 | 1997 |
| The optimality of a fast CNF conversion and its use with SAT P Jackson, D Sheridan Proc. of SAT, 2004 | 16 | 2004 |
| Direct formal verification of liveness properties in continuous and hybrid dynamical systems A Sogokon, PB Jackson International Symposium on Formal Methods, 514-531, 2015 | 14 | 2015 |
| Proving SPARK verification conditions with SMT solvers PB Jackson, GO Passmore Paper regarding the improved results of using SMT-Lib for SPARK, 2009 | 14 | 2009 |
| Constructively formalizing automata RL Constable, PB Jackson, P Naumov, J Uribe Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press …, 1998 | 12 | 1998 |
| Verification of a lazy cache coherence protocol against a weak memory model CJ Banks, M Elver, R Hoffmann, S Sarkar, P Jackson, V Nagarajan 2017 Formal Methods in Computer Aided Design (FMCAD), 60-67, 2017 | 11 | 2017 |
| The NuPRL Proof Development System, Version 4.1 P Jackson Department of Computer Science, Cornell University, 1994 | 10 | 1994 |
| The Cups Game NSF Product Realization Consortium Module Description P Jackson NY: Cornell University, 1996 | 8 | 1996 |
| Gröbner basis construction algorithms based on theorem proving saturation loops GO Passmore, L de Moura, PB Jackson Dagstuhl Seminar Proceedings, 2010 | 7 | 2010 |
Grant Olney PassmoreImandra Inc. and Clare Hall, University of CambridgeVerified email at cl.cam.ac.uk
