16 Aug Seminar August 23 2019: SAT- and SMT-based automated reasoning

Date: Friday 23rd August

Time: 14:15-15.00 NB New Time!

Place: SIRIUS meeting room (8459). 8th Floor, Ole-Johan Dahls hus.

Chi Mai Nguyen, our new postdoctoral researcher at SIRIUS, will present a short introduction about SMT (a technique for deciding the satisfiability of properties expressed as of qualifier-free first order formula) and a brief explanation how to use SMT in problem solving.

Satisfiable Modulo Theories is the problem of deciding the satisfiability of qualifier-free first order formula with respect to some decidable theories. Many efficient SMT solvers were able to handle optimisation problems with up to thousands Boolean/rational variables. It would be a great benefit to exploit the advantage of SMT solvers in problem solving and optimising. This talk gives a short introduction about SMT and a brief explanation how to use SMT in problem solving.

Chi Mai Nguyen is a postdoctoral researcher at the SIRUS centre, Department of Informatics, University of Oslo. She obtained her Master  degree in Theoretical Computer Science at Aalto University, in 2012. In April 2017, she received her PhD degree at University of Trento with the thesis entitled “Efficient Modelling and Reasoning with Constrained Goal Models”. Her work mainly focuses on formal verification, model checking, and applying automated reasoning techniques (mostly SAT and SMT) to goal models. She is a member of the Analysis of Complex Systems research program and will be working in the Integrated Digital Planning beacon.