[ 12 | 11 | 10 | 09 | 08 | 07 | 06 | 05 | 04 | 03 ]

This is a list of some recent public talks.

Talks 2012

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

Hardware Model Checking Competition 2012 (HWMCC'12).
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,
Sept.~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.