Tutorial on SMT and Polynomial Arithmetic

Tutorial dates: May 26-27, 2016
Tutorial location: EDIT 3364 (May 26) and EDIT 8103 (May 27)

Information on Tutorial

The tutorial serves as a crash course in polynomial algebra.

We will first discuss the satisfiability problem modulo various theories, known as the SMT problem.
Then, we will focus on the theory of polynomial arithmetic and introduce decision procedures from polynomial algebra. In particular, we will present decision procesures using Groebner basis computation and quantifier elimination via Cylindrical Algebraic Decomposition.

Tutorial Schedule

There will be 3 lectures, each lecture of 90 minutes. The tentative course schedule is as follows: