Invited talk Yoni Zohar

Title: Satisfiability Modulo Theories in an Undergraduate Class

Yoni Zohar, Bar Ilan University, Israel

Abstract:

Satisfiability Modulo Theories (SMT) solvers are widely used in various applications, most prominently verification of hardware and software. They are focused on the task of checking the satisfiability of first-order formulas over a wide range of background theories. Currently, mainstream SMT-solvers offer easy to use APIs and textual interfaces, and are accessible even to users with little logical background. Nevertheless, their algorithms are based on interesting and varied theoretical subjects.

For these reasons, SMT as a field is a good candidate for introducing automated reasoning and logic to students with little or no background in logic: its wide applicability provides a great motivation to study them, the solvers’ accessibility offers hands-on exercises and the logical foundations contain a wide variety of topics of different levels and depth.

In this talk I will describe my experience in teaching an automated reasoning class focused on SMT. I will describe my original hypotheses and plans before the class, what happened during the class, and some reflections that occurred in the process.