<< BIO
Vitals
US Citizen
Born: 18 October, 1983 {age 35}
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 Co-CEO, Imandra Inc. / Aesthetic Integration (imandra.ai)
- 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.
Funded by NASA Cooperative Agreement NNX08AC59A and by NSF SGER Grant No. CNS-0823086.
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
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-2019}
-
DReaM Group Seminar, University of Edinburgh
July 16th, 2019
I presented an invited talk titled ``An Introduction to the Imandra Automated Reasoning System.''
Mathematical Reasoning Group (DReaM Group), School of Informatics
University of Edinburgh
Edinburgh, Scotland, UK -
Microsoft Research - Visiting Leo de Moura + Invited Talk
May 27th - 31st, 2019
I presented an invited talk titled ``Formal Verification of Financial Algorithms.''
Joint work with Denis Ignatovich, Imandra Inc.
RiSE Group, Microsoft Research
Redmond, Washington, USA -
FMCAD: International Conference on Formal Methods in Computer Aided Design
Oct 30th - Nov 2nd, 2018
I presented an invited talk titled ``Formal Verification of Financial Algorithms in Imandra.''
Joint work with Denis Ignatovich, Aesthetic Integration, Ltd.
University of Texas at Austin
Austin, TX, USA -
CADE: 26th International Conference on Automated Deduction
August 6th - 11th, 2017
I presented an invited talk titled ``Formal Verification of Financial Algorithms.''
Joint work with Denis Ignatovich, Aesthetic Integration, Ltd.
Chalmers University of Technology
Gothenburg, Sweden -
CICM: 10th International Conference on Intelligent Computer Mathematics
July 17th - 21st, 2017
I presented an invited talk titled ``Formal Verification of Financial Algorithms, Progress and Prospects.''
Joint work with Denis Ignatovich, Aesthetic Integration, Ltd.
University of Edinburgh
Edinburgh, Scotland, UK -
Big Proof: Isaac Newton Institute
July 1st - August 4th, 2017
Invited participant in the 2017 Big Proof programme at the Isaac Newton Institute.
University of Cambridge
Cambridge, England, UK -
ACL2: 14th International Workshop on the ACL2 Theorem Prover
May 22nd, 2017
I presented an invited talk titled ``Formal Verification of Financial Algorithms, Progress and Prospects.''
Joint work with Denis Ignatovich, Aesthetic Integration, Ltd.
University of Texas at Austin
Austin, TX, USA -
ITP: Interactive Theorem Proving
August 22nd, 2016
I presented an invited talk titled ``Formal Verification of Financial Algorithms, Progress and Prospects.''
Joint work with Denis Ignatovich, Aesthetic Integration, Ltd.
International Conference on Interactive Theorem Proving
Nancy, France -
AI Now - The White House / NYU Symposium
July 7th, 2016
Invited participant in The White House / NYU Symposium ``AI Now: Social and Economic Implications of Artificial Intelligence Technology in the Near-Term.''
Office of Science and Technology Policy, Executive Office of President Barack Obama
NYU Information Law Institute
Skirball Center for the Performing Arts
New York, NY, USA -
Seven on Seven
May 14th, 2016
Invited participant in the 2016 Rhizome Seven on Seven Conference
Hito Steyerl and I presented our joint work titled ``The Platform for Political Mathematics.''
Rhizome at the New Museum
New York, NY, USA -
Alan Turing Institute - Algorithm Society Workshop
February 17th - 18th, 2016
Invited participant in the Alan Turing Institute's Algorithm Society Workshop
Alan Turing Institute
British Library, London, UK -
Ethereum DEVCON1
November 9th, 2015
Denis Ignatovich and I presented a talk titled ``Towards Imandra Contracts: Formal Verification for Ethereum.''
Ethereum Developers Conference
Gibson Hall, London, UK -
25th International Conference on Automated Deduction (CADE-25)
August 4th - 7th, 2015
I presented a talk titled ``Decidability of Univariate Algebra with Predicates for Rational and Integer Powers.''
Freie Universität Berlin
Berlin, Germany -
Cornell Financial Engineering Manhattan
April 8th, 2015
Denis Ignatovich and I presented a talk titled ``Automated Reasoning for Safety and Fairness of Financial Algorithms.''
Operations Research and Information Engineering
Cornell University
New York, USA -
US Securities and Exchange Commission
April 6th, 2015
Denis Ignatovich and I presented an invited talk titled ``Formal Verification: A Way to Ensure the Safety and Fairness of Financial Algorithms.''
SEC Division of Economic and Risk Analysis
Washington, DC, USA - Queen Mary Theory Seminar
September 10th, 2014
I presented a talk (joint with Leo de Moura) titled ``Exact Global Optimization on Demand.''
Research Group in Theoretical Computer Science
Queen Mary, University of London
London, England, UK - 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).
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
Publicity and Web Chair
- International Conference on Automated Deduction (CADE-2013)
Reviewing: Journals and Books
- Formal Methods in System Design (2015)
- 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
- ‹PC› International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC-2015)
- ‹PC› Conference on Intelligent Computer Mathematics (CICM-2015)
- International Conference on Computer Aided Verification (CAV-2014)
- ‹PC› Conference on Intelligent Computer Mathematics (CICM-2014)
- ‹PC› International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC-2014)
- 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-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› International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC-2013)
- ‹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)
Home Sweet Home
| I grew up mostly upon the idyllic Oyster Creek in Sugar Land, Texas. |
 |