Talks Armin Biere

List of some recent public talks.

Talks 2017

Invited talk
Challenges in Verifying Arithmetic Circuits Using Computer Algebra
19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'17)
Timisoara, Romania, September 2017.

Tutorial on SAT
joint CP'17, ICLP'17, and SAT'17
Melbourne, Australia, August 2017.

Revisiting Decision Diagrams for SAT
Workshop on Pragmatics of Constraint Reasoning (PoCR'17)
Melbourne, Australia, August 2017.

Talks 2016

Invited talk
Decision Heuristics and Restarts in SAT
Deduktionstreffen 2016,
Alpen-Adria-Universität,
Klagenfurt, Austria, September 2016.

Hardware Model Checking Competition
ARM Research Summit 2016,
Cambridge, UK, September 2016.

Weaknesses of CDCL Solvers
Theoretical Foundations of SAT Solving Workshop,
The Fields Institute, University of Toronto,
Toronto, Canada, August 2016.

Translating into SAT
SAT’16 Industrial Day,
Université de Bordeaux,
Bordeaux, France, July 2016.

Splatz SAT Solver
7th Workshop on Pragmatics of SAT (POS'16),
Université de Bordeaux,
Bordeaux, France, July 2016.

Talks 2015

Model Checking, SAT and Bit-Vectors.
Seminar Theoretical Computer Science,
KTH Royal Institute of Technology, Stockholm, Sweden,
Nov. 2015.

Invited talk
HVC'15 Award
SAT Solving for Model Checking and Beyond.
11th Haifa Verification Conference 2015
IBM Research, Haifa, Israel,
Nov. 2015.

Hardware Model Checking Competition 2015 (HWMCC'15).
14th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'15),
Austin, TX, USA,
September 2015.

Evaluating CDCL Variable Scoring Schemes.
18th Intl. Conf. on Theory and Applications of Satisfiability (SAT'15),
Austin, TX, USA,
September 2015.

Evaluating CDCL Restart Schemes.
6th Workshop on Pragmatics of SAT (POS'15),
SAT 2015, Austin, TX, USA,
September 2015.

Parallel SAT Solving or To Share or Not To Share.
Dagstuhl Seminar 15171 on Theory and Practive of SAT Solving,
Shloss Dagstuhl, Leibniz Zentrum für Informatik,
Dagstuhl, Wadern, Germany,
April 2015.

Talks 2014

Invited tutorial
Challenges in Bit-Precise Reasoning, (video)
joined tutorial FMCAD'14 and MEMOCODE'14,
EPFL, Laussanne, Switzerland,
Oct. 2014.

SAT Based Model Checking,
Clarke Symposium 2014, Celebrating 25 Years of Model Checking,
Carnegie Mellon University, Pittsburgh, USA,
September 2014.

Hardware Model Checking Competition 2014 CAV Edition (HWMCC'14).
26th th Intl. Conf. on Computer-Aided Verification (CAV'14),
FLoC Olympic Games 2014, Vienna Summer of Logic,
Vienna, Austria, July 2014.

Invited talk
Lingeling Essentials - Design and Implementation Aspects,
5th Workshop on Pragmatics of SAT (POS'14),
SAT 2014, FloC 2014, Vienna Summer of Logic
July 2014.

Where does SAT not work? (video)
Workshop on Theoretical Foundations of Applied SAT Solving.
Banff International Research Station for Mathematical Innovation and Discovery.
related CACM editorial on this workshop,
Banff, Canada.
Jan. 2014.

Talks 2013

Modbat: A Model-based API Tester for Event-driven Systems.
Haifa Verification Conference (HVC'13),
Haifa, Israel
Nov. 2013.

Hardware Model Checking Competition 2013 (HWMCC'13).
12th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'13),
Portland, Oregon, USA
Oct. 2013.

Simulating Structual Reasoning on the CNF-Level.
First Symposium on Structure in Hard Combinatorial Problems (SSHCP'13),
Vienna, Austria,
May 2013.

Talks 2012

Automated Reencoding of Boolean Formulas.
8th Intl. Haifa Verification Conference,
IBM Research Labs, Haifa, Israel,
Nov. 2012.

Hardware Model Checking Competition 2012 (HWMCC'12).
11th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'12),
Cambridge, UK
Oct. 2012.

Slides presented during a panel on Model Checking in the Cloud,
at 11th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'12),
Cambridge, UK
Oct. 2012.

Understanding Modern SAT Solvers,
5th Summer School on Verification Technology, Systems & Applications (VTSA'12),
Max Planck Institut Informatik, Saarbrücken, Germany,
September 2012.

Invited talk
Practical Aspects of SAT Solving,
SMT'12, PAAR'12
Manchester, UK,
July 20012.

Modern CDCL SAT Solvers,
Second Intl. SAT / SMT Summer School 2012,
Trento, Italy,
June 20012.

Modern SAT Solvers (Part A, Part B),
Winter School on Verification,
Vienna, Austria,
February 2012.

Talks 2011

Invited talk
Preprocessing and Inprocessing Techniques in SAT,
7th Intl. Haifa Verification Conference,
IBM Research Labs, Haifa, Israel,
December 2011.

Hardware Model Checking Competition 2011 (HWMCC'11).
11th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'11),
Austin, TX, USA,
Nov. 2011.

Invited talk
Preprocessing and Inprocessing Techniques in SAT,
Third Workshop on Kernelization (WorKer'11),
Vienna University of Technology, Austria,
September 2011.

SAT-based Model Checking,
First Intl. SAT/SMT Summer School 2011,
MIT, Cambridge, USA,
June 2011.

Unhiding Redundancy in SAT,
Deduction at Scale 2011,
Ringberg Castle, Tegernsee, Germany,
March 2011.

Using High Performance SAT and QBF Solvers, (tptpa11satdemo.zip)
Theorem Proving Tools for Program Analysis (TPTPA'11),
Tutorial co-located with POPL'11,
Austin, Texas, USA,
January 2011.

Talks 2010

Extending the BTOR Language,
Synthesis, Verification, and Analysis of Rich Models (SVARM'10),
Edinburgh,
July 2010.

Tutorial on Decision Procedures in Hardware Design,
Dagstuhl Seminar 10161
Decision Procedures in Software, Hardware and Bioware,
Schloss Dagstuhl, Germany,
April 2010.

Talks 2009

Lazy Hyper Binary Resolution,
Dagstuhl Seminar 09461
Algorithms and Applications for Next Generation SAT Solvers,
Schloss Dagstuhl, Germany,
November 2009.

Introduction to Bounded Model Checking,
FATS: Formal Approaches To Software,
Seminar series at ETH Zürich,
October 2009.

Invited talk
SAT, SMT and Applications
10th Intl. Conf. on Logic Programming and Nonmonotonic Reasoning (LPNMR'09),
Potsdam, Germany,
September 2009.

Minimizing Learned Clauses,
12th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'09),
Swansea, Wales, UK,
July 2009.

Talks 2008

Consistency Checking of All Different Constraints over Bit-Vectors within a SAT-Solver.
8th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'08),
Portland, Oregon, USA,
November 2008.

Hardware Model Checking Competition (HWMCC'08).
20th Intl. Conf. on Computer-Aided Verification (CAV'08),
Princeton, USA,
July 2008.

Tutorial on Model Checking: Modelling and Verification in Computer Science.
Algebraic Biology (AB'08),
Schloss Hagenberg,
August 2008.

Linear Algebra, Boolean Rings and Resolution?
Applications of Computer Algebra (ACA'08),
Schloss Hagenberg,
July 2008.

A Short History of SAT Based Model Checking: From Bounded Model Checking to Interpolation.
Seminar Faculty of Information Technology,
Brno University of Technology,
Brno, Czech Republic,
June 2008.

Adaptive Restart Control for Conflict Driven SAT Solvers,
NVSIDS in action: prime65537fl.mpg (video presented in the talk).
11th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'08),
Guangzhou, P.R. China,
May 2008.

Talks 2007

Hardware Model Checking Competition (HWMCC'07).
19th Intl. Conf. on Computer-Aided Verification (CAV'07),
Berlin, Germany,
July 2007.

Invited talk
A Short History on SAT Solver Technology and What is Next?
10th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'07),
Lisbon, Portugal,
May 2007,
data (14 MB).

Talks 2006

Local Minimization of And-Inverter Graphs.
2nd Guangzhou Symposium on Satisfiability in Logical-Based Modeling,
Guangzhou, China,
Sep. 2006.

BDDs and Extended Resolution.
2nd Alpine Verification Meeting,
Monte Verità, Ascona, Switzerland,
May 2006.

Reachability Analysis with QBF.
6th Intl. Work. on Designing Correct Circuits (DCC'06),
Vienna, Austria,
March 2006.

Talks 2005

QBF in Formal Verification.
1st Alpine Verification Meeting,
EPFL, Laussanne, Switzerland,
October 2005.

Circuit vs CNF Reasoning for Equivalence Checking.
4th Intl. Equivalence Checking Workshop,
Madonna di Campiglio, Italy,
July 2005.

Applications of Quantified Boolean Formulae Decision Procedures.
Colloquium Dept. Electrical Engineering, Informatics and Mathematics,
University of Paderborn, Germany,
July 2005.

Invited talk
SAT in Formal Hardware Verification.
8th Intl. Conf; on Theory and Applications of Satisfiability Testing (SAT'05),
St. Andrews, Scotland,
June 2005.

SAT & QBF in Formal Verification.
RISC Seminar,
Schloss Hagenberg, Austria,
March 2005.

Talks 2004

Resolve and Expand.
7th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'04),
Vancouver, BC, Canada,
May 2004.

No Need for Liveness Model Checking Algorithms?
Beyond Safety, Intl. Workshop,
Schloss Ringberg, Germany,
April 2004.

Talks 2003

About the SAT Solvers Limmat, Compsat, Funex and the QBF Solver Quantor.
Presentation for the SAT'03 SAT Solver Competition,
Santa Margherita Ligure, Portofino, Italy,
May 2003.