Nikolaj Bjorner is a Guest Professor at TUW
A series of guest lectures on SMT Internals will be held at TU Wien from October 13 to 24.
Dr. Nikolaj Bjorner is a Partner Researcher at Microsoft Research. His main line of work focuses on the development of the SMT constraint solver Z3, created together with Leonardo de Moura, Lev Nachmanson, and Christoph Wintersteiger. Z3 has become one of the most influential tools in automated reasoning, widely applied in program verification, test case generation, formal methods, and other domains that demand rigorous correctness guarantees. The work surrounding Z3 has received several awards. Beyond Z3, Bjorner and Karthick Jayaraman developed SecGuru, a tool used in Microsoft Azure to validate firewalls and routing configurations. In recognition of his contributions to automated reasoning and formal methods, Bjorner was named an ACM Fellow in 2021.
Dr. Nikolaj Bjorner, hosted by Prof. Laura Kovacs, will deliver guest lectures on SMT solving internals. His lectures will provide a comprehensive overview of the theoretical and practical foundations of Satisfiability Modulo Theories (SMT) solving. Topics include CDCL(T) and theory reasoning, quantifier handling, pre- and in-processing techniques, optimization modulo theories, and solving Constrained Horn Clauses. In addition to these conceptual foundations, the course will examine implementation aspects and the internal mechanisms of Z3. By combining theoretical background with practical insights, the course aims to equip participants with a solid understanding of SMT principles and hands-on knowledge of engineering high-performance reasoning tools.
