Board
Chair
olaf.beyersdorff@uni-jena.de
Olaf Beyersdorff is Professor of Theoretical Computer Science at Friedrich Schiller University Jena, Germany. Before coming to Jena in 2018 he spent six years at the University of Leeds (UK), as Professor of Computational Logic (2017-18), Associate Professor (2015-17), and Lecturer (2012-15). He received his PhD from Humboldt University Berlin in 2006.
His research interests are in algorithms, complexity, computational logic, and in particular proof complexity. In the past years he has primarily worked on proof complexity of quantified Boolean formulas (QBF) and its connections to QBF solving. In 2018, he served as co-chair of the SAT conference. He is also Speaker of the Section ‘Logic in Computer Science’ of the German Computer Society (GI).
Vice Chair
Martina.Seidl@jku.at
Martina Seidl is professor at the Johannes Kepler University Linz, Austria. There she chairs the Institute for Symbolic Artificial Intelligence which was founded in 2020. Prior to that, she was first assistant and later associate professor at the Institute for Formal Models and Verification, also at Johannes Kepler University Linz. She holds a PhD from the Vienna University of Technology where she worked several years as a researcher.
Her research interests cover various topics in automated reasoning with a strong focus on solving quantified Boolean formulas. She is also a co-organizer of the QBF competition QBFEval. Furthermore, she works on software verification and on tools for logic education.
Treasurer
mengel@cril.fr
Stefan Mengel is a researcher employed by the French Centre national de la recherche scientifique (CNRS) working at CRIL in Lens, France. He recieved his PhD from the University of Paderborn, Germany. The focus of of his work lies in the intersection of computational complexity theory, algorithms and combinatorics. In recent years he has mostly worked on the theory of knowledge compilation. In particular, he is very interested in applications in database theory and artificial intelligence.
Extended Board Members
Counselor
biere@cs.uni-freiburg.de
Since August 2021 Professor 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. Between 2000 and 2004 he held a position as Assistant Professor within the Department of Computer Science at ETH Zürich, Switzerland. In 1999 Biere was working for a start-up company in electronic design automation after one year as Post-Doc with Edmund Clarke at CMU, Pittsburgh, USA. In 1997 Biere received a Ph.D. in Computer Science from the University of Karlsruhe, Germany. His primary research interests are applied formal methods, more specifically formal verification of hardware and software, using model checking, propositional and related techniques. He is the author and co-author of more than 60 papers and served on the program committee of more than 45 international workshops and conferences. His highest influential work is the contribution to Bounded Model Checking. Decision procedures for SAT, QBF and SMT, developed by him or under his guidance rank at the top of many international competitions. Besides organizing several workshops Armin Biere was co-chair of SAT'06 and FMCAD'09. He is on the editorial board of the Journal on Satisfiability, Boolean Modeling and Computation (JSAT), and is one of the editors of the Handbook of Satisfiability. He also organizes the Hardware Model Checking Competition.
Counselor
john.franco@uc.edu
Professor Franco received a B.S. in Electrical Engineering from the City College of New York in 1969. He was a Member of Technical Staff in the Digital Signal Processing group at Bell Laboratories in Holmdel, New Jersey from 1969 to 1975. He earned a M.S. in Electrical Engineering from Columbia University in New York in 1971 and Ph.D. in Computer Science from Rutgers University in New Brunswick, New Jersey in 1981. He served on the faculties of Case Western Reserve University and Indiana University before coming to the University of Cincinnati in 1990. He is associate editor of the Journal of Satisfiability, Boolean Modeling, and Computation, assistant editor of Annals of Mathematics and Artificial Intelligence, theory editor of the Encyclopedia of Computer Science and Engineering, and has co-edited several special issues of AMAI and Discrete Applied Mathematics. He has served on the steering committee of the annual Symposium on the Theory and Applications of Satisfiability Testing from its beginning as the Workshop on Satisfiability in 1996. He has recently co-organized the Workshop on Satisfiability: Assessing the Progress.
SMT Representative
roberto.sebastiani@unitn.it
My research focuses on Formal Verification (in particular, model checking) and Automated Reasoning (in particular SAT and SMT) and and their applications. My current interests are:
Satisfiability Modulo Theories (SMT) and its applications to Formal verification: SMT is the problem of checking satisfiability of formulas in complex theories which extend boolean satisfiability (typically decidable subclasses of First-order logic). I’m one of the inventors of the ``lazy’’ approach to SMT (now state-of-the-art), which efficiently combines DPLL-based SAT solvers with theory-specific decision procedures. I have investigated and developed many techniques for developing efficient decision procedures for SMT in expressive theories (modal logics, description logics, linear arithmetic on reals and integers) on top of boolean SAT solvers. With my collaborators we have introduced the technique of Delayed Theory Combination as an alternative to “Classic” Nelson-Oppen combination technique for SMT solvers. Variants of this technique is now implemented in all state-of-the-art SMT solvers. We also have introduced the idea of Formal Verification of RTL circuit designs and of timed and hybrid systems based on SMT.
Formal Verification, Model Checking: My research in this field focuses on new techniques for model checking with linear temporal logic (LTL)] and for bounded model checking. With my coauthors, we have proposed for the first time an extension of bounded model checking for the verification of real-time and hybrid systems by means of SMT tools. From an application viewpoint, I have worked on verification of real-word, industrial systems in technology transfer projects by means of model checking techniques.
Formal Reasoning in SW Specification: I have worked on applying automated reasoning techniques (mostly SAT and SMT) to goal models, a formalism used for requirements analysis within the TROPOS SW engineering methodology.
My past research involved also: SAT for non-CNF formulas, Decision procedures for modal and description logics, Planning, and Abstraction in theorem proving.
Auditors
Auditor
jan.johannsen@ifi.lmu.de
Jan Johannsen is a Senior Lecturer and Head of the Department office at the Institute for Informatics of Ludwig-Maximilians-Universität München, Germany. He obtained his doctoral degree in Computer Science in 1996 from FAU Erlangen-Nürnberg, and spent two years as a Postdoc at UC San Diego, before joining LMU Munich in 1999. His research interests are Propositional Proof Complexity, in particular in relation to SAT Solving, and more generally in anything in the intersection of Logic and Computational Complexity.
Auditor
F.Slivovsky@liverpool.ac.uk