team
contact
software
publications
teaching
jobs

[ 21 | 20 | 19 | 18 | 17 | 16 | 15 | 14 | 13 | 12 | 11 | 10 | 09 | 08 | 07 | 06 | 05 | 04 | 03 ]

Talks Armin Biere

List of some recent public talks.

Invited
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 2⁵ 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