<< BIO

Vitals

US Citizen
Born: 18 October, 1983 {age 30}
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 Positions
  • Co-Founder and CEO, Aesthetic Integration, London
  • Principal, Imandra Capital Group Limited, Guernsey
  • Life Member, Clare Hall, University of Cambridge
  • Honorary Associate, LABORES - Laboratoire de Recherche Scientifique, Paris

(Recent) Previous Positions

{October, 2010 - April, 2014}
   Researcher on Cambridge-Edinburgh EPSRC grant Automatic Proof Procedures for Polynomials and Special Functions

{October, 2010 - April, 2014}
   Research Associate, LFCS, University of Edinburgh

{December, 2010 - December, 2012}
   Postdoctoral Associate in Metamathematics of Real Algebraic Geometry, Clare Hall, University of Cambridge

{July - December, 2012}
   Visiting Scientist with André Platzer, Logical Systems Laboratory, Carnegie Mellon University

{January - July, 2012}
   Programme Participant, SAS: A Legacy of Alan Turing, Isaac Newton Institute for Mathematical Sciences, Cambridge, England

{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 Area: Automated Theorem Proving and Algorithmic Algebraic Geometry
PhD Supervisor: Dr. Paul B. Jackson
Mathematical Reasoning Group & Algorithms and Complexity Group
Laboratory for Foundations of Computer Science (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
Advisor: Jaap van Oosten
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-2014}

  • MAP: Mathematics = Algorithms + Proofs
    May 26-30th, 2014
    I presented an invited talk (joint with Leo de Moura) titled ``Exact Global Optimization on Demand.''
    IHP Trimester on Semantics of Proofs and Certified Mathematics
    Institut Henri Poincaré
    Paris, France

  • DPMMS, Cambridge - Departmental Talk
    April 24th, 2014
    I presented a talk titled ``Computing Downward Lowenheim-Skolem: Hands on with the Real Algebraic Numbers.''
    Dept of Pure Mathematics and Mathematical Statistics (DPMMS)
    University of Cambridge
    Cambridge, England, UK

  • Royal Society International Seminar: Computational Interpretations of Mathematical Theorems
    November 25-26th, 2013
    Kavli Royal Society International Centre
    The Royal Society at Chicheley Hall
    Buckinghamshire, England, UK

  • COST Action Meeting - EU Rich Model Toolkit Working Group
    October 17th, 2013
    I presented a talk (joint with Leo de Moura) titled ``Exact Global Nonlinear Optimization on Demand.''
    IMDEA Software Institute
    Madrid, Spain

  • Schloss Dagstuhl Seminar on Deduction and Arithmetic
    October 6th - 8th, 2013
    I presented a talk (joint with Leo de Moura) titled ``Exact Global Optimization on Demand.''
    Schloss Dagstuhl - Leibniz-Zentrum für Informatik
    Dagstuhl, Germany

  • SIAM Conference on Applied Algebraic Geometry
    August 1st - 4th, 2013
    I presented a talk (joint with Leo de Moura) titled ``Automatic Proofs for Transcendental Function Inequalities and an Application to Global Optimization.''
    Colorado State University
    Fort Collins, Colorado, USA

  • 24th International Conference on Automated Deduction (CADE-24)
    June 9th - 14th, 2013
    Leo de Moura presented a talk on our joint work titled ``Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals.''
    Lake Placid, NY, USA

  • Automated Deduction: Decidability, Complexity, Tractability (ADDCT-2013)
    June 10th, 2013
    I presented a talk (joint with Leo de Moura) titled ``(Exact Global Nonlinear) Optimization on Demand.''
    Co-located with CADE-24
    Lake Placid, NY, USA

  • Edinburgh Mathematical Reasoning Group (DReaM Talk)
    May 14th, 2013
    I presented a talk (joint with Leo de Moura) titled ``Some Unexpected Applications of Nonstandard Models.''
    Mathematical Reasoning Group
    University of Edinburgh
    Edinburgh, Scotland, UK

  • Reproducibility in Computational and Experimental Mathematics
    December 14th, 2012
    Jeremy Avigad presented a talk (including our joint work on logic in SAGE) called ``Interactive Theorem Proving, Automated Reasoning, and Mathematical Computation.''
    Institute for Computational and Experimental Research in Mathematics (ICERM)
    Brown University
    Providence, Rhode Island, USA

  • CMACS Seminar on Real Algebra and Hybrid Systems
    September - December, 2012
    I gave a series of lectures on real algebra and decision procedures over real closed fields and transcendental extensions.
    Logical Systems Laboratory
    Carnegie Mellon University
    Pittsburgh, Pennsylvania, USA

  • Conference on Intelligent Computer Mathematics
    July 8th - 13th, 2012
    I presented a talk (joint with Larry Paulson and Leo de Moura) titled ``Real Algebraic Strategies for MetiTarski Proofs.''
    Jacobs University
    Bremen, Germany

  • International Workshop on Strategies in Rewriting, Proving and Programming
    July 1st, 2012
    I presented a talk (joint with Leo de Moura) titled ``The Strategy Challenge in SMT Solving.''
    Part of IJCAR, 2012
    University of Manchester
    Manchester, England

  • Computability in Europe 2012: Turing Centenary Conference
    June 19th, 2012
    I presented a talk (joint with Paul Jackson) titled ``Abstract Partial Cylindrical Algebraic Decomposition I: The Lifting Phase.''
    University of Cambridge
    Cambridge, England

  • SAT/SMT Summer School 2012
    June 12th - 15th, 2012
    Fondazione Bruno Kessler
    Trento, Italy

  • Robin Milner Symposium 2012
    April 15th - 18th, 2012
    University of Edinburgh
    Edinburgh, Scotland

  • 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).
    Microsoft Research Redmond
    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.
    Southwestern Center for Arithmetical Algebraic Geometry
    University of Arizona
    Tucson, AZ, USA

  • Logic for Automated Reasoning and Automated Reasoning for Logic (LARARL-2006)
    June 8th-12th, 2006  Cancelled
    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

Publicity and Web Chair

  • International Conference on Automated Deduction (CADE-2013)

Reviewing: Journals and Books

  • Annals of Mathematics and Artificial Intelligence (2014)
  • Theoretical Computer Science (2013)
  • ACM Transactions on Mathematical Software (2012, 2013)
  • Journal of Automated Reasoning (2009, 2011, 2012)
  • International Journal of Computer Science and Technology (2012)
  • Journal of Symbolic Computation (2011)
  • New Computational Paradigms (2007)

Reviewing: Conferences and Workshops

  • International Symposium on Symbolic and Algebraic Computation (ISSAC-2013)
  • International Conference on Automated Deduction (CADE-2013)
  • ‹PC› International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS-2013)
  • ‹PC› International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC-2012, SYNASC-2013)
  • NASA Formal Methods Symposium (NFM-2013)
  • International Colliquium on Automata, Languages and Programming (ICALP-2013)
  • International Conference on Formal Engineering Methods (ICFEM-2012)
  • ‹PC› Symposium on Integration of Symbolic Computation and Mechanised Reasoning (Calculemus-2011)
  • ‹PC› 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› 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.