|
|
Board
| |
|
| ♦ |
|
Chair |
| |
|
|
Olaf Beyersdorff
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
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 |
| |
Stefan Mengel
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 |
| |
Armin Biere
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
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
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
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 |
| |
Florian Lonsing
lonsing@cs.stanford.edu
|
| |
Florian Lonsing is currently a research scientist in Clark Barrett's group in the
Computer Science Department at Stanford University, which he joined in
2019.
His current research focuses on theoretical and practical aspects of
hardware verification in a broad sense. He is also particularly
interested in quantified Boolean formulas (QBF), proof systems and
decision procedures for QBFs, applications, preprocessing, and
automated reasoning.
From 2012 to 2018, he was a postdoctoral researcher in the
Knowledge-Based Systems Group in the Institute of Logic and
Computation at TU Wien, Austria. Previously, from 2008 to 2012, he was
research and teaching assistant and doctoral student at the Institute
of Formal Models and Verification at Johannes Kepler University in
Linz, Austria. |
|
| |
|
|
| | | |
