PhD Students

  • Kristjan Liiva, University of Edinburgh (2013-). Co-supervised with Dr Paul B. Jackson, Edinburgh.

    Kristjan is working on decision methods in real algebra and analysis, with a special interest in the design and application of SMT-oriented decision procedures for nonlinear real arithmetic. In July, 2014, he will begin receiving support from Microsoft Research, Cambridge, with Christoph Wintersteiger as his MSR mentor.

Recent Taught or Supervised Courses

  • Decision Procedures for Nonlinear Arithmetic, a one-week mini-course in Maria Paola Bonacina's MSc Automated Reasoning course, Autumn 2014, Università degli Studi di Verona. Click here for mini-course resources.

  • CMACS Seminar on Real Algebra and Hybrid Systems (joint with André Platzer), Autumn 2012, Logical Systems Lab, Carnegie Mellon University, Pittsburgh, USA.

  • Decision Methods over Real and Algebraically Closed Fields, Lent (Spring) 2012, Department of Pure Mathematics and Mathematical Statistics, University of Cambridge.

  • Supervision for Glynn Winskell's Discrete Mathematics, Lent (Spring) 2012, Computer Laboratory, University of Cambridge.


    . .
    : ::.
    : ::::.

{Expository notes}

Sums of Squares Positivstellensatzen Methods Explained: Part I

Understanding Algebro-Geometric Quantifier Elimination: Part I, Algebraically Closed Fields of Characteristic Zero via Muchnik