<< BIO
Vitals
US Citizen
Born: 18 October, 1983 {age 28}
Erdös number: 3 {Passmore --> Gurevich --> Shelah --> Erdös}
My Academic Family Tree (where `parent' means `Ph.D. supervisor'), extracted from The Mathematics Genealogy Project
Current Research Positions
- Researcher on Cambridge-Edinburgh EPSRC
grant Automatic Proof Procedures for Polynomials and Special
Functions
- Postdoctoral Associate, Clare Hall, University of Cambridge
- Research Associate, LFCS, University of Edinburgh
- Honorary Associate, LABORES - Laboratoire de Recherche Scientifique, Paris
- Programme Participant, Semantics and Syntax: A Legacy of Alan Turing, Isaac Newton Institute for Mathematical Sciences, Cambridge, England {January - July, 2012}
(Recent) Previous Research Positions
{January, 2011}
Visiting Researcher with Yuri Gurevich, Microsoft Research [FSE],
Redmond, Washington, USA
{September, 2007 - October, 2010}
PhD Student of Paul B. Jackson, LFCS and Mathematical Reasoning Group,
University of Edinburgh, Scotland
{April, 2010}
Visiting Researcher with Florent Kirchner, INRIA/IRISA [CELTIQUE],
Rennes, Bretagne, France
{April - June, 2009}
Research Intern with Leo de Moura, Microsoft Research [SRR],
Redmond, Washington, USA
{May - October, 2008}
Visiting Fellow with N. Shankar and Sam Owre, SRI International [FMDS],
Menlo Park, California, USA
Education
PhD, University of Edinburgh {2011}
PhD
Dissertation: Combined Decision Procedures for Nonlinear
Arithmetics, Real and Complex
PhD Supervisor: Dr. Paul
B. Jackson
Mathematical Reasoning Group and Algorithms and
Complexity Group
LFCS, School of Informatics
PhD Examiners: Dr. Daniel Kroening (Oxford) and Dr. Alan Smaill (Edinburgh)
Master Class, Mathematical Research Institute in The Netherlands
{2007}
Project: Abstract Properties of Partial Combinatory Algebras
Administered by Department of
Mathematics, Universiteit Utrecht &
Department of Mathematics,
Katholieke Universiteit Nijmegen
BA, University of Texas at Austin {2007}
Honors Thesis: Diophantine Sets and Their Decision Problems
Thesis Advisor: Prof. Dr. Robert S. Boyer
Department of Mathematics
Lectures Given and Scientific Participation {2004-2012}
- Semantics and Syntax: A Legacy of Alan Turing (SAS) Programme
January 19th, 2012
I presented a talk titled ``Decision Methods over Real and Algebraically Closed Fields.''
Isaac Newton Institute for Mathematical Sciences
Cambridge, England - Visiting Jeremy Avigad at Carnegie Mellon University
December 12th - 17th, 2011
Pittsburgh, Pennsylvania, USA - Visiting Leonardo de Moura at Microsoft Research, Redmond
December 7th - 11th, 2011
Redmond, Washington, USA -
Dulles High School Math and Science Academy
December 6th, 2011
I presented a talk titled ``On the Mathematical Experience'' to my high school alma mater!
Sugar Land, Texas, USA -
17th International Conference on Principles and Practice of Constraint Programming
September 14th, 2011
Leonardo de Moura presented a talk on our joint work titled ``Orchestrating Decision Engines.''
Perugia, Italy -
18th International Symposium on Fundamentals of Computation Theory
August 22-25, 2011
Yuri Gurevich presented a lecture on our joint work titled ``Impugning Randomness, Convincingly.''
University of Oslo
Oslo, Norway -
CUNY Logic Seminar
March 22nd, 2011
Yuri Gurevich presented a seminar on our joint work titled ``Impugning Randomness, Convincingly.''
Graduate Center CUNY
New York, New York, USA -
Deduction at Scale
March 8th, 2011
Paul B. Jackson presented a talk on our joint work titled ``Improved Techniques for Proving Nonlinear Arithmetic Problems.''
Ringberg Castle
Max Planck Society
Tegernsee, Germany -
Deduction at Scale
March 7th, 2011
Leonardo de Moura presented a talk on our joint work titled ``Orchestrating Decision Engines.''
Ringberg Castle
Max Planck Society
Tegernsee, Germany -
Cambridge Automated Reasoning Group Lunch
February 22nd, 2011
I presented a talk titled ``The Strategy Challenge in Computer Algebra.''
Computer Laboratory
University of Cambridge
Cambridge, England, UK -
Galois, Inc. Tech Talk
February 7th, 2011
I presented a talk titled ``The Strategy Challenge in Computer Algebra.''
Galois, Inc.
Portland, Oregon, USA -
Principia Mathematica 100th Anniversary Symposium
November 27-28th, 2010
Trinity College
University of Cambridge
Cambridge, England, UK - Trusted Extensions of Interactive Theorem Provers
August 11-12th, 2010
I presented (joint with Paul B. Jackson and Florent Kirchner) a talk titled ``Thoughts on Trusting RAHD Computations.''
University Centre
University of Cambridge
Cambridge, England, UK - Logics for System Analysis
Co-located with LICS and IJCAR (FLoC)
July 15th, 2010
I presented (joint with Paul B. Jackson) an introductory tutorial titled ``Combined Decision Techniques for the Existential Theory of the Reals.''
I presented (joint with Florent Kirchner) a talk titled ``Thinking Outside the (Arithmetic) Box: Certifying RAHD Computations.''
University of Edinburgh
Edinburgh, Scotland, UK - LFCS Lab Lunch
July 6th, 2010
I presented a talk titled ``Some Recent Work on SAT Modulo Nonlinear Real Arithmetic.''
University of Edinburgh
Edinburgh, Scotland, UK - Game-theoretic Probability and Related Topics
June 21st - 23rd, 2010
I presented a talk (joint with Yuri Gurevich) titled ``Towards Algebraic Descriptive Randomness.''
Royal Holloway, University of London
London, England, UK - Dagstuhl Seminar on Decision Procedures in Hardware, Software, and Bioware
April 18-23rd, 2010
I presented a talk (joint with Leo de Moura and Paul B. Jackson) titled ``Abstract Groebner Bases and Some Applications in Z3 and RAHD.''
Here is a photograph!
Schloss Dagstuhl - Leibniz Center for Informatics
Dagstuhl, Germany - INRIA/IRISA Team Celtique Seminar
April 2nd, 2010
I presented a talk (joint with Leo de Moura and Paul B. Jackson) titled ``Abstract Groebner Bases and Nonlinear Arithmetic in SMT.''
INRIA/IRISA Bretagne
Rennes, Bretagne, France - Scottish Theorem Proving Seminar
November 20th, 2009
I presented a talk (joint with Leo de Moura) titled ``Recent Advances in SAT Modulo Nonlinear Real Arithmetic.''
University of Edinburgh,
Scotland, UK - SYNASC 2009 (11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing)
September 26th - 29th, 2009
I presented a talk (joint with Leo de Moura) titled ``Superfluous S-polynomials in Strategy-independent Groebner Bases.''
West University, Timisoara, Romania,
RISC Linz, Johannes Kepler University, Austria, and
Research Institute e-Austria Timisoara
Timisoara, Transylvania, Romania - SMT 2009 (SATisfiability Modulo Theories)
co-located with CADE 2009 (Conference on Automated Deduction)
August 2nd, 2009
I presented a talk (joint with Leo de Moura) titled ``On Locally Minimal Nullstellensatz Proofs.''
McGill University
Quebec, Montreal, Canada - ADDCT 2009 (Automated Deduction: Decidability, Complexity, Tractability)
co-located with CADE 2009 (Conference on Automated Deduction)
August 2nd, 2009
I presented a talk (joint with Leo de Moura) titled ``Universality of Polynomial Positivity and a Variant of Hilbert's 17th Problem.''
McGill University
Quebec, Montreal, Canada - Calculemus 2009: 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning
July 7th, 2009
I presented a talk (joint with Paul B. Jackson) titled ``Combined Decision Techniques for the Existential Theory of the Reals.''
Work appears in the book ``Intelligent Computer Mathematics'' published by Springer-Verlag.
Grand Bend, Ontario, Canada - MSR Internship Final Talk
June 26th, 2009
I presented a talk titled ``Some Results on Nonlinear Arithmetic Helpful to Z3.''
The results covered can be found in two joint papers by Leo de Moura and myself:- ``On Locally Minimal Nullstellensatz Proofs'' (in SMT-2009; pdf),
- ``Superfluous S-polynomials in Strategy-Independent Groebner Bases'' (in submission; pdf).
Redmond, WA, USA - Verification Working Group
April 16th, 2009
I presented a talk titled ``A High-level Sketch of the RAHD (`Real Algebra in High Dimensions') Decision Method.''
See here for an abstract of my talk.
Microsoft Research Redmond
Redmond, WA, USA - Workshop on Linking Formal Design and Verification Tools to
Create Trustworthy Software
Nov 27-28th, 2008
I presented two posters (both joint with Paul Jackson): Microsoft Research Cambridge
Cambridge, England, UK
- SRI Computer Science Laboratory Seminar
October 30th, 2008
I presented a talk titled ``RAHD: A Feasible Decision Method for Real Algebra in High Dimensions.''
See here for an abstract of my talk.
SRI International
Menlo Park, CA, USA - Summer School Marktoberdorf 2008 - Engineering Methods and Tools for Software Safety and Security
August 5-17th, 2008
An Advanced Study Institute of the NATO Science for Peace and Security Programme, and
The Institut für Informätik, Technische Universitat München
Marktoberdorf, Germany - SRI Formal Methods and Dependable Systems Group Talk
I presented a talk titled ``Decision Methods for the Existential Theory of Real Closed Fields.''
June 27th, 2008
SRI International
Menlo Park, CA, USA - Formal Methods Outreach Workshop
June 9-10th, 2008
SRI International
Menlo Park, CA, USA - CAMELEON - Cambridge-Leeds-Norwich Logic and Set Theory Meeting
April 23rd, 2008 (a post-action shot!)
I presented a talk titled ``A Family of Decidable Nonlinear Fragments of the True Existential Theory of the Rational Number Field.''
Centre for Mathematical Sciences
Department of Pure Mathematics and Mathematical Statistics
University of Cambridge
Cambridge, England, UK - BCTCS-2008 - 24th British Colloquium for Theoretical Computer Science
April 7-10th, 2008 (an action shot!)
I presented a talk titled ``Open Euclidean Relations and Decidable Fragments of the True Existential Theory of the Rational Number Field.''
Grey College at Durham University
Banquet at Durham Castle (pretty!)
Durham, England, UK - TTVSI - A Festschrift in Honour of Prof. Michael J. C. Gordon FRS
March 25-26th, 2008
Paul Jackson and I presented a short talk and poster on our joint work titled ``A Continuous Relaxation for Proving Discrete ACL2 Theorems over Real Closed Fields.''
The Royal Society
London, England, UK - IDT Talk: Edinburgh Interdisciplinary Tea Seminar
March 17th, 2008
I presented a talk titled ``Isolating Decidable Nonlinear Fragments of Undecidable Number Theories.''
See here for more information.
Department of Informatics
University of Edinburgh
Edinburgh, Scotland, UK
- CAMELEON - Cambridge-Leeds-Norwich Logic and Set Theory Meeting
December 11th, 2007
Department of Mathematics
University of East Anglia
Norwich, England, UK
- ACL2 Theorem Prover Workshop 2007
November 15-16th, 2007
Matt Kaufmann, Jacob Kornerup, and Mark Reitblatt presented a ``Rump Session'' talk on our joint work centered around using the ACL2 theorem prover to prove properties of programs written in the graphical parallel dataflow programming language LabVIEW/G.
Jeff Kodosky, the inventor of LabVIEW and founder of our theorem proving project, gave a Keynote Address on his vision for the future of our project.
Note: I was sadly not able to be there in person.
Co-located with FMCAD-2007
Austin, TX, USA
- DReaM Talk: Edinburgh Mathematical Reasoning Group
October 5th, 2007
I presented a talk titled ``Hilbert's Tenth Problem and Some Weak Relatives.''
See here for an abstract of my talk.
Mathematical Reasoning Group
University of Edinburgh
Edinburgh, Scotland, UK - MAP (Mathematics: Algorithms and Proofs)
January 8-12th, 2007
The Lorentz Center
Universeteit Leiden
Leiden, The Netherlands
- CAMELEON Cambridge-Leeds-Norwich Logic and Set Theory Meeting and CL Minicourse on Countable Ordinals
November 29th - December 2nd, 2006
Center for Mathematical Sciences, and
Computer Laboratory
University of Cambridge
Cambridge, England, UK
- PSSL-84 (Peripatetic Seminar on Sheaves and Logic)
October 14-15th, 2006
Institut fur Theoretische Informatik
Technical University of Braunschweig
Braunschweig, Germany
- Association for Symbolic Logic Annual Conference
Special Goedel Centennial Meeting
May 17-21st, 2006
Universite du Quebec a Montreal
Montreal, Quebec, Canada
- N.I.TECH - National Instruments Corp. Annual Technical Conference
April 7th, 2006
Dr. Jacob Kornerup and I presented a talk titled ``How LabVIEW and its Theorem Prover Help You Build Absolutely Reliable Systems.''
National Instruments Corporation - Main Campus
Austin, TX, USA
- College of Natural Sciences' Undergraduate Research Forum
April 7th, 2006
I presented my work titled ``Proof Theory in Proof Theory: A Computational Relativisation of Hilbert's Program.''
Under the auspices of the Department of Computer Sciences and the Department of Mathematics
College of Natural Sciences, Welch Hall Forum
University of Texas at Austin
Austin, TX, USA - Arizona Winter School in Computational and Algorithmic Aspects of Algebra and Arithmetic
March 11th-15th, 2006
Special courses in:- integer factorization,
- explicit methods for solving Diophantine equations,
- computing cohomology in algebraic geometry,
- and discriminants, resultants, and their tropicalization.
University of Arizona
Tucson, AZ, USA - Logic for Automated Reasoning and Automated Reasoning for Logic (LARARL-2006)
June 8th-12th, 2006Cancelled
I am on the programme committee. Click here for CfP.
Part of The International Computer Science Symposium in Russia (CSR-2006)
St. Petersburg Department of Steklov Institute of Mathematics, &
Euler International Mathematical Institute
St. Petersburg, Russia - UT Austin ACL2 Seminar
October 19th, 2005 (one day after my 22nd birthday!)
I presented a talk titled "Automated Reasoning in LabVIEW with the Method/ACL2 System."
A short abstract can be found here.
Dept. of Computer Sciences / ACL2 Group
University of Texas, Austin
Austin, TX, USA - Argonne Workshop on Automated Reasoning and Deduction (AWARD-2005)
August 11-13, 2005
I presented a talk titled "Automated Reasoning in LabVIEW and Some Elementary Thoughts on Proof Theoretic Techniques for Automating Interpretability."
Mathematics and Computer Science Division
Argonne National Laboratory
University of Chicago
Chicago, IL, USA - Topics in Graduate Mathematics: Summer Workshop in Proof Theory
June 6 - June 17th, 2005
University of Notre Dame
Southbend, IN, USA
Group Photo! - Austin Center for Advanced Studies Annual Conference
April 2005
IBM Austin Center for Advanced Studies
Austin, TX, USA
- Association for Symbolic Logic Annual Conference
March 2005
Stanford University
Palo Alto, CA, USA
- Association for Symbolic Logic Annual Conference
May 2004
Carnegie Mellon University
Pittsburgh, PA, USA
Reviewing and Professional Service
Journals and Books
- Journal of Symbolic Computation (2011)
- Journal of Automated Reasoning (2009, 2011)
- New Computational Paradigms (2007)
Conferences and Workshops
- ‹PC member› Symposium on Integration of Symbolic Computation and Mechanised Reasoning (Calculemus-2011)
- ‹PC member› Computer Algebra in Computer-Aided Design and Verification (CAV-CA-2011)
- Formal Methods in Computer-Aided Design (FMCAD-2010)
- Symposium on Integration of Symbolic Computation and Mechanised Reasoning (Calculemus-2009)
- Frontiers of Combining Systems (FRoCoS-2009)
- Theorem Proving in Higher-Order Logics (TPHOLS-2008)
- Computer Science Logic (CSL-2008)
- ‹PC member› Logic for Automated Reasoning and Automated Reasoning for Logic (LARARL-2006)
- Logic for Programming Artificial Intelligence and Reasoning (LPAR-2005)
Memberships in Professional Socieities
The Edinburgh Mathematical Society
The American Mathematical Society
The Mathematical Association of America
The Association for Symbolic Logic
The Association for Computability in Europe
The Computability and Complexity in Analysis Network
The Association for Automated Reasoning
The Association of Lisp Users
The Association for Advancement of Artificial Intelligence
Foundations of Mathematics (FOM)
Cambridge and Edinburgh
| I am very lucky to be working in two of the most magical cities in the world. | |
 Cambridge, England photo by Kevin Allen |  Edinburgh, Scotland photo by JuanJ (Flickr) |
Home Sweet Home
| I grew up mostly upon the idyllic Oyster Creek in Sugar Land, Texas. |
 |