|
Board
| |
|
♦ |
|
Chair |
| |

Fahiem Bacchus
fbacchus@cs.toronto.edu |
| |
Fahiem Bacchus is a Professor of Computer Science at the University of
Toronto. His research fits broadly in the area of Knowledge Representation
and Reasoning, a sub-field of Artificial Intelligence. He has made a
number of key contributions during his career, including the development
of logics for representing different forms of probabilistic knowledge and
automated planning algorithms that can exploit domain specific control
knowledge expressed in Linear Temporal Logic (LTL). For the past 15
years his work has concentrated on automated reasoning algorithms for
solving various forms of the satisfiability problem: finding a model
(SAT), counting the number of models (#SAT), solving quantified Boolean
formulas (QBF), and finding optimal models (MaxSat). His group has been
successful in building award winning solvers for all of these problems. He
has served as the Program Chair of several major AI conferences, including
UAI-2005, SAT-2005; and and as Conference Chair of IJCAI-2017. Fahiem
is also a Fellow of the Association for the Advancement of AI (AAAI).
|
|
| |
|
♦ |
|
Vice Chair |
| |

Armin Biere
armin.biere@jku.at |
| |
Since 2004 Prof. Armin Biere chairs 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.
|
|
| |
|
♦ |
|
Treasurer |
| |

Hans Kleine Büning
kbcsl@upb.de
|
| |
Hans Kleine Büning received the Doctor Rerum Naturalium
from Westfälische Wilhelms-Universität Münster in 1977.
Prof. Dr. Büning has made important contributions to understanding
connections between Computer Science and Logic, especially in the
areas of function equivalence and quantified Boolean formulas. He is
co-author of Aussagenlogik: Deduktion und Algorithmen, with
Theodor Lettmann (1994), which was translated to English as
Propositional logic: deduction and algorithms in 1999. He was a
co-founder of the successful series Workshop on Satisfiability
which later became the International Conference on the Theory and
Practice of Satisfiability Testing.
|
|
| |
|
Extended Board Members
| |
|
♦ |
|
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 |
| |

Uwe Egly
uwe@kr.tuwien.ac.at
|
| |
My research interests are
proof theory and proof complexity, knowledge representation and reasoning, computational logic, satisfiability checking for QBFs, argumentation an argumentation frameworks, algorithm for pathplanning, application of AI methods in engineering.
|
|
| |
|
♦ |
|
Auditor |
| |

Carsten Sinz
carsten.sinz@kit.edu
|
| |
I am a computer scientist currently acting as head of the research
group "Verification meets Algorithm Engineering" at the Institute for
Theoretical Computer Science of Karlsruhe Institute of Technology,
Germany. Before that, I have been a member of the Symbolic Comptuation
Group at the University of Tübingen, Germany and the Institute for
Formal Models and Verification at the Johannes Kepler University Linz,
Austria. I studied computer science and physics at the Eberhard Karls
University Tübingen, Germany, where I gratuated with a PhD (Dr. rer.
nat.) in computer science.
My professional interests include SAT Solving (especially industrial
applications, parallel SAT algorithms, and visualization of SAT
instances), Product Configuration (modeling and verification issues),
and Software Verification (bounded model checking).
Over the last years, I have also been working on different industry
projects on software verification and product configuration with
DaimlerChrysler, IBM, Siemens, and T-Systems.
|
|
| |
|
|
| | | |