SAT-based Model-Checking

We gave an overview of SAT-based model checking checking, starting from bounded model checking and a small examples for bit-blasting. We discussed safety, liveness and fairness checking, before turning towards completeness issues. We looked at complete algorithm, including k-induction, its incremental implementation, deductive model checking, interpolants for model checking, and finally at a simplified version of property driven reachability.

Armin Biere, Johannes Kepler University, Linz, Austria

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.