Tutorial Presenters

Armin Biere

University of Freiburg

Quantum Leaps and Local-Search

Brief Bio

Armin Biere is leading the Chair of Computer Architecture at the Albert-Ludwigs-University Freiburg in Germany after 17 years as head of the Institute for Formal Models and Verification at the Johannes Kepler University in Linz, Austria. His primary research interests are applied formal methods, more specifically formal verification of hardware and software, using model checking and related techniques with the focus on developing efficient SAT and SMT solvers. He is the author and co-author of more than 220 papers and served on the program committee of more than 160 international conferences and workshops. His most influential work is his contribution to Bounded Model Checking. Decision procedures for SAT, QBF and SMT, developed by him or under his guidance rank at the top many international competitions and were awarded 104 medals including 57 gold medals. He is a recipient of an IBM faculty award in 2012, received the TACAS most influential paper in the first 20 years of TACAS award in 2014, the HVC'15 award on the most influential work in the last five years in formal verification, simulation, and testing, the ETAPS 2017 Test of Time Award, the CAV Award in 2018, the IJCAI-JAIR 2019 Award, and the 1990s Most Influential Paper Award at DAC'23.

Alexander Nadel

Intel, Haifa and Faculty of Data and Decision Sciences, Technion

Introduction to SAT

Brief Bio

Alexander Nadel is a research scientist and engineer. Alexander has been with Intel since 2003, where he is leading the development of SAT technology (including SAT, MaxSAT, SMT and model checking) and its deployment to automate various tasks in physical design, formal verification, scheduling, and test generation. In 2023, Alexander also joined the Technion as a part-time research fellow. Alexander is the author or co-author of over 35 papers, including the best paper at FMCAD 2010. He has served on the program committee of over 35 conferences and workshops and co-chaired the SMT Workshop in 2021 and the FMCAD 2023 conference. Open-source solvers developed by Alexander have won the SAT Competition and MaxSAT Evaluation several times.

Friedrich Slivovsky

University of Liverpool

An Introduction to QBF Solving

Brief Bio

Friedrich Slivovsky is a lecturer in computer science at the University of Liverpool. He holds a PhD from TU Wien (Vienna), where he also completed a postdoctoral fellowship. His research focuses on propositional satisfiability (SAT) and its generalizations, such as quantified Boolean formulas (QBF).