Por Mikolas Janota (Professor Auxiliar Convidado, DI/FCUL).

Resumo: Quantification permeates mathematical logic and its applications. SW and HW verification are prominent examples where in certain properties quantification is indispensable. Further, quantification is tightly connected to two-player games and function synthesis. In this talk we will look at algorithms for solving Quantified Boolean Formulas (QBFs). We will also mention some theoretical results separating the different QBF algorithms as well as the connection between QBF and SMT with quantification.

Short Bio: Mikolas did his MSc at the Charles University in Prague and his PhD at University College Dublin.
He continued as a PostDoc and later as researcher at INESC-ID, Lisboa. Before starting as a visiting professor at FCUL he was a PostDoc at MSR Cambridge UK. Mikolas has a longstanding interest in logic and its applications, such as product configuration and software verification. In the recent years he has mainly focused on solving logic problems that involve quantification---quantified boolean formulae (QBF) in particular. At MSR he has participated in development of the SMT solver Z3.