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 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 96 medals including 55 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 in 2014 award, 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, and the IJCAI-JAIR 2019 Award.

Besides organizing several workshops Armin Biere was co-chair of SAT'06, and FMCAD'09, was PC co-chair of HVC'12, co-chair of CAV'14, and acted as co-chair of TACAS'20. He serves on the editorial boards of the Journal on Satisfiability, Boolean Modeling and Computation (JSAT), the Journal of Automated Reasoning (JAR), the journal for Formal Methods in System Design (FMSD) and as Associate Editor of the Journal of Artificial Intelligence Research (JAIR).

He is an editor of the Handbook of Satisfiability and initiated and organizes the Hardware Model Checking Competition (HWMCC). From 2011-2017 he served as chair and from 2017 to 2020 as vice-chair of the SAT Association and since 2012 on the steering committee of FMCAD. In 2006 Armin Biere co-founded NextOp Software Inc. which was acquired by Atrenta Inc. in 2012.

Since February 2014 Prof. Armin Biere acts as chair of student affairs (Präses) for computer science, helping to organize the PhD program in computer science. During the same time until May 2015 he also acted as head of the commission of the curriculum committee (Studienkommissionsvorsitzender) for the bachelor and master program in computer science and thus was as well responsible for admission and credit transfer, for both the bachelor and master program in computer science.


Science Park 3, 2nd Floor, North-East Wing
+43 732 2468 4541
Room 0248


Publications and Talks are listed on seperate pages. You may also be interested in software.



Institute for Formal Models and Verification
Johannes Kepler University
Altenbergerstr. 69
4040 Linz