Prof. Dr. Armin Biere
Head of Group
 |
|
Biographical Sketch
Since August 2021 Professor Armin Biere is leading the Chair of Computer Architecture at the 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 279 papers and served on the program committee of more than 206 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 107 medals including 60 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 award in 2014, 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, the IJCAI-JAIR 2019 Award, the 1990s Most Influential Paper Award at DAC'23, and the Herbrand Award at IJCAR'24.
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, acted as co-chair of TACAS'20. He served on the editorial boards of the Journal of Automated Reasoning (JAR) (2011 to 2021) and the journal for Formal Methods in System Design (FMSD) (2012 - 2021). From 2019 to 2023 he filled the role of Associate Editor on the Journal of Artificial Intelligence Research (JAIR) and continues to serve on the editorial board of Journal on Satisfiability, Boolean Modeling and Computation (JSAT) since its inception in 2004, and since summer 2023 as editor in chief.
He is an editor of the Handbook of Satisfiability, for the first edition in 2009 and the second edition in 2021, and initiated and organizes the Hardware Model Checking Competition (HWMCC) from 2007-2024. From 2011-2017 he served as (first) chair and from 2017 to 2020 as vice-chair, now as counselor to the board of the SAT Association. Since 2012 he is a member of the steering committee of FMCAD. In 2006 Armin Biere co-founded NextOp Software Inc. which was acquired by Atrenta Inc. in 2012.
From 2014 to 2021 until he moved to Freiburg Prof. Armin Biere acted as chair of student affairs (Präses) for computer science, helping to organize the PhD program in computer science at JKU. 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.
Since October 2023 he acts as director of the Informatics Institute Freiburg (IIF), the department of computer science at the University of Freiburg.
Publications
2020 ]
2021 |
2022 |
2023 |
2024 |
2025
2010 ]
2011 |
2012 |
2013 |
2014 |
2015 |
2016 |
2017 |
2018 |
2019
2000 ]
2001 |
2002 |
2003 |
2004 |
2005 |
2006 |
2007 |
2008 |
2009
1990 |
1991 |
1992 |
1993 ]
1994 |
1995 |
1996 |
1997 |
1998 |
1999
[ DBLP | Google Scholar | Semantic Scholar | ORCID | Scopus ]
2025
On Enumerating Short Projected Models
Sibylle Möhle, Roberto Sebastiani, Armin Biere
Discrete Applied Mathematics (DAM)
vol. 361,
pages 412-439,
Elsevier 2025
[ paper
| bibtex
| doi
]
2024
SAT Solving for Variants of First‑Order Subsumption
Robin Coutelier,
Jakob Rath,
Michael Rawson,
Armin Biere,
Laura Kovács
Formal Methods in System Design
Springer 2024, published online
[ paper
| bibtex
| doi
]
Clausal Equivalence Sweeping
Armin Biere,
Katalin Fazekas,
Mathias Fleury,
Nils Froleyks
Proc. 24th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'24)
page 236-241,
TU Wien Academic Press
2024
[ paper
| bibtex
| slides
| doi
| kissat
| hwmcc20miters
| hwmcc12miters
| experiments
]
Hardware Model Checking Competition 2024
Armin Biere,
Nils Froleyks,
Mathias Preiner
Proc. 24th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'24)
page 7,
TU Wien Academic Press
2024
[ paper
| bibtex
| competition
| slides
| doi
]
CaDiCaL, Gimsatul, IsaSAT and Kissat Entering the SAT Competition 2024
Armin Biere,
Tobias Faller,
Katalin Fazekas,
Mathias Fleury,
Nils Froleyks
and
Florian Pollitt
Proc. SAT Competition 2024: Solver, Benchmark and Proof Checker Descriptions
Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2024-1,
pages 8-10,
University of Helsinki 2024
[ paper
| bibtex
| cadical
| isasat
| kissat
| gimsatul
| medals
]
Challenging Combinational Hardware Equivalence Checking Problems Submitted to the SAT Competition 2024
Armin Biere,
Tobias Faller,
Katalin Fazekas,
Mathias Fleury,
Nils Froleyks
and
Florian Pollitt
Proc. SAT Competition 2024: Solver, Benchmark and Proof Checker Descriptions
Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2024-1,
page 33,
University of Helsinki 2024
[ paper
| bibtex
]
Dynamic Blocked Clause Elimination for Projected Model Counting
Jean-Marie Lagniez,
Pierre Marquis and
Armin Biere.
Proc. 27th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'24)
Leibniz International Proceedings in Informatics (LIPIcs)
vol. 305,
pages 21:1-21:17
Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2024
[ paper
| bibtex
| slides
| doi
]
Clausal Congruence Closure
Armin Biere, Katalin Fazekas,
Mathias Fleury and
Nils Frolekys
Proc. 27th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'24)
Leibniz International Proceedings in Informatics (LIPIcs)
vol. 305,
pages 6:1-6:25
Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2024
[ paper
| preprint
| bibtex
| slides
| doi
]
CaDiCaL 2.0
Armin Biere,
Tobias Faller
Katalin Fazekas,
Mathias Fleury,
Nils Froleyks and
Florian Pollitt
Proc. Computer Aided Verification - 26th Intl. Conf. (CAV'24)
Lecture Notes in Computer Science (LNCS)
vol. 14681,
pages 133-152,
Springer 2024
[ paper
| bibtex
| official
| artifact
| cadical
| doi
]
Certifying Phase Abstraction
Nils Froleyks,
Emily Yu,
Armin Biere and
Keijo Heljanko
Proc. Automated Reasoning - 12th Intl. Joint Conf. (IJCAR'24)
Lecture Notes in Computer Science (LNCS)
vol. 14739,
pages 284-303,
Springer 2024
[
doi |
paper |
bibtex |
extended |
arxiv |
certifaiger
]
Certifying Incremental SAT Solving
Katalin Fazekas, Florian Pollitt,
Mathias Fleury and
Armin Biere
Proc. 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'24)
EasyChair Proceedings and Collections (EPIC)
vol. 100,
pages 321-340,
Easychair 2024
[ paper
| bibtex
| lidrup-check
| idrup-check
| cvc5-branch
| cvc5-modifications
| cadical-version
]
Certified SAT solving with GPU accelerated Inprocessing
Muhammad Osama, Anton Wijs and Armin Biere
Formal Methods in System Design
vol. 62(1),
pages 79-118,
Springer 2024
[ paper
| bibtex
| parafrost
| doi
]
Incremental Proofs for Bounded Model Checking
Katalin Fazekas, Florian Pollitt,
Mathias Fleury and
Armin Biere
Proc. 27th GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems
(MBMV'24)
ITG Fachberichte
vol. 314,
pages 133-143,
VDE Verlag 2024
[ preprint
| bibtex
]
Ternary Simulation as Abstract Interpretation (Work in Progress)
Nils Froleyks, Emily Yu and Armin Biere
Proc. 27th GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems
(MBMV'24)
ITG Fachberichte
vol. 314,
pages 148-151,
VDE Verlag 2024
[ preprint
| bibtex
]
Disjoint Partial Enumeration without Blocking Clauses
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
Proc. 38th AAAI Conference on Artificial Intelligence (AAAI'24)
pages 8126 - 8135, AAAI Press 2024
[ preprint
| doi
| zenodo
]
2023
BIG Backbones
Nils Froleyks,
Emily Yu and
Armin Biere
Proc. 23rd Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'23)
pages 162-167,
TU Wien Academic Press
2023
[
paper |
bibtex |
doi |
kb3 |
benchmarks
]
Towards Compositional Hardware Model Checking Certification
Emily Yu,
Nils Froleyks and
Armin Biere
Proc. 23rd Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'23)
pages 44-54,
TU Wien Academic Press
2023
[
paper |
bibtex |
doi |
chmc |
certifaiger
]
The SAT Museum
Armin Biere,
Mathias Fleury,
Nils Froleyks and
Marijn Heule
Proc. 14th Intl. Workshop on Pragmatics of SAT (POS'23)
CEUR Workshop Proceedings
vol. 3545,
pages 72-87,
CEUR-WS.org 2023
[ paper
| bibtex
| data
| zenodo
| ceur
]
Uncovering and Classifying Bugs in MaxSAT Solvers through Fuzzing and Delta Debugging
Tobias Paxian and
Armin Biere
Proc. 14th Intl. Workshop on Pragmatics of SAT (POS'23)
CEUR Workshop Proceedings
vol. 3545,
pages 59-71,
CEUR-WS.org 2023
[ paper
| bibtex
| data
| ceur
]
Armin Biere,
Mathias Fleury and
Florian Pollitt
CaDiCaL_vivinst, IsaSAT, Gimsatul, Kissat, and TabularaSAT Entering
the SAT Competition 2023
Proc. SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions
Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2023-1,
pages 14-15,
University of Helsinki 2023
[ paper
| bibtex
]
Verifying Floating-Point Commutativity with GRS
Robin Trüby,
Mathias Fleury and
Armin Biere
Proc. SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions
Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2023-1,
page 53,
University of Helsinki, 2023
[ paper
| bibtex
]
Faster LRAT Checking Than Solving with CaDiCaL
Florian Pollitt,
Mathias Fleury and
Armin Biere
Proc. 26th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'23)
Leibniz International Proceedings in Informatics (LIPIcs)
vol. 271,
pages 21:1-21:12,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2023
[ paper
| bibtex
]
Highlighted paper
IPASIR-Up: User Propagators for CDCL
Katalin Fazekas,
Aina Niemetz,
Mathias Preiner,
Markus Kirchweger,
Stefan Szeider and
Armin Biere
Proc. 26th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'23)
Leibniz International Proceedings in Informatics (LIPIcs)
vol. 271,
pages 8:1-8:13,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2023
[ paper
| bibtex
| zenodo
| sms
| cvc5
| cadical
]
CadiBack: Extracting Backbones with CaDiCaL
Armin Biere,
Nils Froleyks
and Wenxi Wang
Proc. 26th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'23)
Leibniz International Proceedings in Informatics (LIPIcs)
vol. 271,
pages 3:1-3:12,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2023
[ paper
| bibtex
| cadiback
| benchmarks
]
ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving
Maximilian Heisinger,
Martina Seidl
and
Armin Biere
Proc. 29th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23)
Lecture Notes in Computer Science (LNCS)
vol. 13993,
pages 426-447,
Springer 2023
[ paper
| doi
| bibtex
| paracooba
]
Improving AMulet2 for Verifying Multiplier Circuits using SAT Solving and Computer Algebra
Daniela Kaufmann and
Armin Biere
International Journal on Software Tools for Technology Transfer (STTT)
vol. 25(2),
pages 133-144,
Springer 2023
[ paper
| doi
| bibtex ]
Efficient Proof Checking with LRAT in CaDiCaL (Work in Progress)
Florian Pollitt,
Mathias Fleury,
and Armin Biere
Proc. 26th GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems
(MBMV'23)
ITG Fachberichte
vol. 309,
pages 64-67,
VDE Verlag 2023
[
paper |
bibtex
]
Emily Yu,
Nils Froleyks,
Armin Biere and
Keijo Heljanko
Stratified Certification for k-Induction (Extended Abstract)
Proc. 26th GMM/ITG/GI Workshop on Methods and Description Languages for Modelling and Verification of Circuits and Systems
(MBMV'23)
ITG Fachberichte
vol. 309,
pages 68-69,
VDE Verlag 2023
[
paper |
bibtex |
certifaiger
]
2022
First-Order Subsumption via SAT Solving
Jakob Rath,
Armin Biere,
Laura Kovács
Proc. 22nd Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'22)
pages 160-169,
TU Wien Academic Press
2023
[ paper
| bibtex
| doi
]
Practical Algebraic Calculus and Nullstellensatz with the Checkers Pacheck and Pastèque and Nuss-Check
Daniela Kaufmann,
Mathias Fleury,
Armin Biere and
Manuel Kauers
Formal Methods in System Design
Springer 2022
[ preprint
| bibtex
| doi
]
Mining Definitions in Kissat with Kittens
Mathias Fleury and
Armin Biere
Formal Methods in System Design
vol. 60(3),
pages 381-404,
Springer 2022
[ preprint
| bibtex
| paper
| data
| doi
]
Emily Yu,
Nils Froleyks,
Armin Biere and
Keijo Heljanko
Stratified Certification for k-Induction
Proc. 22nd Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'22)
pages 59-64,
TU Wien Academic Press
2022
[
paper |
bibtex |
certifaiger
]
Better Decision Heuristics in CDCL through Local Search and Target Phases
Shaowei Cai,
Xindi Zhang,
Mathias Fleury and
Armin Biere
Journal of Artificial Intelligence Research (JAIR)
vol. 74,
pages 1515-1563,
2022
[ paper
| doi
| bibtex
| code
| data
]
QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers
Maximilian Heisinger,
Martina Seidl and
Armin Biere
Proceedings of the Workshop on Practical Aspects of Automated Reasoning (PAAR'22)
CEUR Workshop Proceedings
vol. 3201,
CEUR-WS.org 2022
[ paper
| bibtex
| quapi
| ceur
]
Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses
Mathias Fleury
and
Armin Biere
CoRR abs/2207.13577 (2022)
presented at
POS'22
[ paper
| arxiv
| bibtex
| gimsatul
| slides
]
Gimsatul, IsaSAT and Kissat entering the SAT Competition 2022
Armin Biere and
Mathias Fleury
Proc. of SAT Competition 2022 - Solver and Benchmark Descriptions
Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2022-1,
pages 10-11,
University of Helsinki 2022
[ paper
| bibtex
]
Hardware Model Checking Certificates
Emily Yu,
Nils Froleyks,
Armin Biere and
Mathias Fleury
In Proc. of SAT Competition 2022 - Solver and Benchmark Descriptions
Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2022-1,
page 46,
University of Helsinki 2022
[ paper
| bibtex
]
Migrating Solver State
Armin Biere,
Md Solimul Chowdhury,
Marijn J. H. Heule,
Benjamin Kiesl
and Michael W. Whalen
Proc. 25th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'22)
Leibniz International Proceedings in Informatics (LIPIcs)
vol. 236,
pages 21:1-21:24,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2022
[ preprint
| doi
| bibtex
| migrating CaDiCaL source code
]
Fuzzing and Delta Debugging And-Inverter Graph Verification Tools
Daniela Kaufmann and Armin Biere
Proc. 16th Intl. Conf. on Tests and Proofs (TAP'22)
Lecture Notes in Computer Science (LNCS)
vol. 13361,
pages 69-88,
Springer 2022
[ preprint
| bibtex
| artifact
| amulet
]
Clausal Proofs for Pseudo-Boolean Reasoning
Randal E. Bryant,
Armin Biere and
Marijn J. H. Heule
Proc. 28th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Lecture Notes in Computer Science (LNCS)
vol. 13243,
pages 443-461,
Springer 2022
[ paper
| bibtex
| github
| zenodo
]
Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
Daniela Kaufmann,
Paul Beame, Armin Biere,
and Jakob Nordström
Proc. Design, Automation and Test in Europe (DATE'22)
IEEE 2022
[ paper
| bibtex
| experiments
]
2021
Single Clause Assumption without Activation Literals to Speed-up IC3
Nils Froleyks and Armin Biere
Proc. 21st Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'21)
pages 72-76,
TU Wien Academic Press
2021
[
paper |
bibtex |
experiments |
cadical
]
Decomposition Strategies to Count Integer Solutions over Linear Constraints
Cunjing Ge and
Armin Biere
Proc. 30th Intl. Joint Conf. on Artificial Intelligence (IJCAI'21)
pages 1389-1395, ijcai.org 2021
[ paper
| bibtex
]
Preprocessing in SAT Solving
Armin Biere,
Matti Järvisalo and
Benjamin Kiesl
Handbook of Satisfiability (2nd ed.)
Frontiers in Artificial Intelligence and Applications
Chapter 9,
vol. 336,
pages 391-435,
IOS Press 2021
[
manuscript |
bibtex |
ebook
]
Bounded Model Checking
Armin Biere
Handbook of Satisfiability (2nd ed.)
Frontiers in Artificial Intelligence and Applications
Chapter 18,
vol. 336,
pages 739-764,
IOS Press 2021.
[
manuscript |
bibtex |
ebook
]
AMulet 2.0 for Verifying Multiplier Circuits
Daniela Kaufmann and
Armin Biere
Proc. 27th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Lecture Notes in Computer Science (LNCS),
vol. 12652,
pages 357-364,
Springer 2021
[ paper
| bibtex
| artifact
]
CaDiCaL, Kissat, Paracooba Entering the SAT Competition 2021
Armin Biere,
Mathias Fleury and
Maximillian Heisinger
Proc. of SAT Competition 2021 - Solver and Benchmark Descriptions
Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2021-1,
pages 10-13,
University of Helsinki 2021
[ paper
| bibtex
| cadical
| kissat
| paracooba
]
CNF Encodings of Complete Pairwise Combinatorial Testing of our SAT Solver Satch
Armin Biere
Proc. of SAT Competition 2021 - Solver and Benchmark Descriptions
Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2021-1,
page 46,
University of Helsinki 2021
[ paper
| bibtex
]
SAT Solving with GPU Accelerated Inprocessing
Muhammad Osama,
Anton Wijs and
Armin Biere
Proc. 14th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21)
Lecture Notes in Computer Science (LNCS),
vol. 12651,
pages 131-151,
Springer 2021
[ paper
| bibtex
| parafrost
]
Efficient All-UIP Learned Clause Minimization
Mathias Fleury and
Armin Biere
Proc. 24rd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'21)
Lecture Notes in Computer Science (LNCS)
pages 171-187,
volume 12831,
Springer 2021
[ preprint
| extended
| bibtex
| experiments
| video
]
Efficient All-UIP Learned Clause Minimization (Extended Version)
Mathias Fleury and
Armin Biere
FMV Reports Series,
Institute for Formal Models and Verification
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria
Technical Report 21/3,
May 2021
[ report
| bibtex
| doi
]
XOR Local Search for Boolean Brent Equations
Wojciech Nawrocki,
Zhenjun Liu,
Andreas Fröhlich,
Marijn J.H. Heule and
Armin Biere
Proc. 24th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'21)
Lecture Notes in Computer Science (LNCS)
pages 417-435,
volume 12831,
Springer 2021
[ preprint
| bibtex
| slides
| recording
| benchmarks
| satch
| cnf2xnf
| xnfsat
]
Progress in Certifying Hardware Model Checking Results
Emily Yu,
Armin Biere and
Keijo Heljanko.
Proc. 24rd Computer Aided Verification (CAV'21)
Lecture Notes in Computer Science (LNCS)
pages 363-386,
volume 12760,
Springer 2021
[ paper
| bibtex
| certifaiger
]
Non-clausal Redundancy Properties
Lee Barnett and
Armin Biere
Proc. 28th International Conference on Automated Deduction(CADE 28)
Lecture Notes in Computer Science (LNCS)
pages 252-272,
volume 12699,
Springer 2021
[ paper
| extended
| bibtex
| dxddcheck
]
Non-Clausal Redundancy Properties (Extended Version)
Lee Barnett and
Armin Biere
FMV Reports Series,
Institute for Formal Models and Verification
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria
Technical Report 21/2, April 2021
[ report
| bibtex
| doi
]
Program Analysis Benchmarks Submitted to the Model Counting Competition MC 2020
Sibylle Möhle,
Cunjing Ge and
Armin Biere
FMV Reports Series,
Institute for Formal Models and Verification
Johannes Kepler University
Altenbergerstr. 69, 4040 Linz, Austria
Technical Report 21/1, January 2021
[ report
| bibtex
| doi
]
2020
The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus
Daniela Kaufmann, Mathias Fleury, Armin Biere
Proc. Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'20)
6 pages,
IEEE 2020
[ paper
| bibtex
| experiments
]
The SAT Practitioner's Manifesto
Armin Biere,
Matti JIärvisalo,
Daniel Le Berre,
Kuldeep Meel,
Stefan Mengel
Version 1.0, Zenodo Sep.~2020
[ paper
| bibtex
| github
| video
| doi
]
Tutorial on Word-Level Model Checking
Armin Biere
Proc. Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'20)
1 page,
IEEE 2020
[ paper
| bibtex
| slides
]
Duplex Encoding of Staircase At-Most-One Constraints for the Antibandwidth Problem
Katalin Fazekas, Markus Sinnl, Armin Biere, Sophie Parragh
Proc. 17th Intl. Conf. on Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR'20)
Lecture Notes in Computer Science (LNCS)
vol. 12296,
pages 186-204,
Springer 2020
[ preprint
| bibtex
| experiments
]
Nullstellensatz-Proofs for Multiplier Verification
Daniela Kaufmann, Armin Biere
Proc. Computer Algebra in Scientific Computing (CASC'20)
Lecture Notes in Computer Science (LNCS)
vol. 12291,
pages 368-389,
Springer 2020
[ paper
| bibtex
| experiments
]
CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the SAT Competition 2020
Armin Biere,
Katalin Fazekas, Mathias Fleury, Maximillian Heisinger
Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions
Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2020-1,
pages 50-53,
University of Helsinki, 2020
[ paper
| bibtex
| kissat
| cadical
| paracooba
| plingeling
| treengeling
]
Duplex Encoding of Antibandwidth Feasibility
Katalin Fazekas, Markus Sinnl, Armin Biere, Sophie Parragh
Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions
Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors)
Department of Computer Science Report Series B
vol. B-2020-1,
pages 81-82,
University of Helsinki, 2020
[ paper
| bibtex
| benchmarks
]
Four Flavors of Entailment
Sibylle Möhle, Roberto Sebastiani, Armin Biere
Proc. 23rd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'20)
Lecture Notes in Computer Science (LNCS)
vol. 12178,
pages 62-71,
Springer 2020
[ preprint
| bibtex
]
Distributed Cube and Conquer with Paracooba
Maximilian Heisinger, Mathias Fleury,
Armin Biere
Proc. 23rd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'20)
Lecture Notes in Computer Science (LNCS)
vol. 12178,
pages 114-122,
Springer 2020
[ preprint
| bibtex
| award
| experiments
| paracooba
]
Covered Clauses Are Not Propagation Redundant
Lee Barnett, David Cerna, Armin Biere
Proc. 10th Intl. Joint Conf. on Automated Reasoning (IJCAR'20)
Lecture Notes in Computer Science (LNCS)
vol. 12166,
pages 32-47,
Springer 2020
[ preprint
| bibtex
]
Computational Logic in the First Semester of Computer Science: An Experience Report
David Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger,
Armin Biere
Proc. 12th Intl. Conf. on Computer Supported Education (CSEDU'20)
pages 374-381,
SCITEPRESS 2020
[ preprint
| bibtex
]
Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App
David Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger,
Armin Biere
Proc. ACM Conf. on Innovation and Technology in Computer Science Education (ITiCSE'20)
pages 61-67,
ACM 2020
[ preprint
| bibtex
]
From DRUP to PAC and Back
Daniela Kaufmann, Armin Biere, Manuel Kauers
Proc. Design, Automation and Test in Europe (DATE'20)
pages 654-657,
IEEE 2020
[ paper
| bibtex
| experiments
]
Strong Extension-Free Proof Systems
Marijn Heule, Benjamin Kiesl, Armin Biere
Journal of Automated Reasoning
64(3),
pages 533-554,
Springer 2020
[ preprint
| bibtex
| experiments
]
Simulating Strong Practical Proof Systems with Extended Resolution
Benjamin Kiesl, Adrián Rebola-Pardo, Marijn Heule, Armin Biere
Journal of Automated Reasoning
64(7),
pages 12247-1267,
Springer 2020
[ paper
| bibtex
| drat2er
| pr2drat
| data
]
SAT, Computer Algebra, Multipliers
Daniela Kaufmann, Armin Biere, Manuel Kauers
Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops
pages 1-18,
EasyChair 2020
[ paper
| bibtex
]
Incremental column-wise verification of arithmetic circuits using computer algebra
Daniela Kaufmann, Armin Biere, Manuel Kauers
Journal of Formal Methods in System Design
vol. 56(1),
pages 22-54,
Springer 2020
[ preprint
| bibtex
| experiments
]
2019
Benjamin Kiesl , Marijn Heule, Armin Biere.
Truth Assignments as Conditional Autarkies.
To be published in Proc. 17th Intl. Symp. on Automated Technology for Verification and Analysis (ATVA'19),
Lecture Notes in Computer Science (LNCS),
vol. 11781,
pages 48-64,
Springer 2019.
[ preprint
| bibtex
| source
]
Daniela Kaufmann, Armin Biere, Manuel Kauers.
Verifying Large Multipliers by Combining SAT and Computer Algebra.
In Proc. 19th
Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'19),
pages 28-36,
IEEE 2019.
[ preprint
| bibtex
| experiments
]
Best poster and interaction award
Sibylle Möhle, Armin Biere.
Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting.
In Proc. 5th Intl. Global Conf. on Artificial Intelligence (GCAI'19),
EasyChair Proceedings and Collections (EPIC),
vol. 71,
pages 1-18,
EasyChair 2019.
[ preprint
| award
]
Best student paper
Katalin Fazekas, Armin Biere, Christoph Scholl.
Incremental Inprocessing SAT Solving.
In Proc. 22nd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'19),
Lecture Notes in Computer Science (LNCS),
vol. 11628,
pages 136-154,
Springer 2019.
[ preprint
| bibtex
| experiments
| pictures
]
Sibylle Möhle, Armin Biere.
Backing Backtracking
In Proc. 22nd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'19),
Lecture Notes in Computer Science (LNCS),
vol. 11628,
pages 250-166,
Springer 2019.
[ preprint
| bibtex
| experiments
]
Armin Biere.
CaDiCaL at the SAT Race 2019.
In Proc. of SAT Race 2019 - Solver and Benchmark Descriptions,
Marijn Heule, Matti Järvisalo, Martin Suda (editors),
vol. B-2019-1 of Department of Computer Science Series of Publications B,
pages 8-9,
University of Helsinki,
2019.
[ paper
| bibtex
]
Mate Soos, Armin Biere.
CryptoMiniSat 5.6 with YalSAT at the SAT Race 2019.
In Proc. of SAT Race 2019 - Solver and Benchmark Descriptions,
Marijn Heule, Matti Järvisalo, Martin Suda (editors),
vol. B-2019-1 of Department of Computer Science Series of Publications B,
pages 14-15,
University of Helsinki,
2019.
[ paper
| bibtex
]
Daniela Kaufmann, Manuel Kauers, Armin Biere, David Cok.
Arithmetic Verification Problems Submitted to the SAT Race 2019.
In Proc. of SAT Race 2019 - Solver and Benchmark Descriptions,
Marijn Heule, Matti Järvisalo, Martin Suda (editors),
vol. B-2019-1 of Department of Computer Science Series of Publications B,
pages 49,
University of Helsinki,
2019.
[ paper
| bibtex
]
Marijn Heule, Benjamin Kiesl, Armin Biere.
Clausal Proofs of Mutilated Chessboards.
In Proc. 11th Intl. Symp. NASA Formal Methods (NFM'19),
Lecture Notes in Computer Science (LNCS),
vol. 11460,
pages 204-210
[ preprint
| bibtex
| experiments
]
Nominated best paper
Marijn Heule, Benjamin Kiesl, Armin Biere.
Encoding Redundancy for Satisfaction-Driven Clause Learning.
In Proc. 25th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19),
Lecture Notes in Computer Science (LNCS),
vol. 11427,
pages 41-58
[ preprint
| bibtex
| experiments
]
2018
Sibylle Möhle, Armin Biere.
Dualizing Projected Model Counting.
To be published in Proc. 30th Intl. Conf. on Tools with Artificial Intelligence (ICTAI'18),
8 pages,
IEEE Computer Society, 2018.
[ paper
| dualiza
]
Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere.
Local Redundancy in SAT: Generalizations of Blocked Clauses.
Logical Methods in Computer Science,
vol. 9,
issue 4:3,
pages 1-23,
https://lmcs.episciences.org
2018.
[ paper
| bibtex
]
Armin Biere, Daniel Kröning.
SAT-Based Model Checking.
In Handbook of Model Checking,
Springer 2018.
[ paper
| bibtex
]
Marijn Heule, Oliver Kullmann, Armin Biere.
Cube-and-Conquer for Satisfiability.
In Handbook of Parallel Constraint Reasoning,
Springer 2018.
[ paper
| bibtex
]
Armin Biere.
CaDiCaL, Lingeling, Plingeling, Treengeling and
YalSAT Entering the SAT Competition 2018.
In Proceedings of SAT Competition 2018 - Solver and Benchmark Descriptions,
Marijn Heule, Matti Järvisalo, Martin Suda (editors),
vol. B-2018-1 of Department of Computer Science Series of Publications B,
pages 13-14,
University of Helsinki,
2018.
[ paper
| bibtex
]
Armin Biere.
Divider and Unique Inverse Benchmarks Submitted to the SAT Competition 2018.
In Proceedings of SAT Competition 2018 - Solver and Benchmark Descriptions,
Marijn Heule, Matti Järvisalo, Martin Suda (editors),
vol. B-2018-1 of Department of Computer Science Series of Publications B,
page 56,
University of Helsinki,
2018.
[ paper
| bibtex
]
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2018.
Technical Report 18/1, Stanford University and
FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria,
June 2018.
[ report
| bibtex
| boolector
]
Daniela Ritirc, Armin Biere, Manuel Kauers.
A Practical Polynomial Calculus
for Arithmetic Circuit Verification.
In
Proc. 3rd Intl. Workshop on Satisfiability Checking and Symbolic Computation (SC2'18),
pages 61-76,
CEUR-WS, 2018.
[ paper
| bibtex
| experiments
]
Katalin Fazekas, Fahiem Bacchus, Armin Biere.
Implicit Hitting Set Algorithms for Maximum Satisfiability
Modulo Theories.
In Proc. 9th Intl. Joint Conf. on Automated Reasoning (IJCAR'18),
Lecture Notes in Computer Science (LNCS),
vol. 10900,
pages 134-151,
Springer 2018.
[ paper
| bibtex
]
Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere.
Btor2, BtorMC and Boolector 3.0.
In Proc. 30th Intl. Conf. on Computer Aided Verification (CAV'18),
Lecture Notes in Computer Science (LNCS),
vol. 10981,
pages 587-595,
Springer 2018.
[ paper
| bibtex
| btor2tools
| boolector
| experiments
]
Adrian Rebola Pardo, Armin Biere.
Two flavors of DRAT.
In Proc. 9th Work. on Pragmatics of SAT 2015 and 2018,
EasyChair Proceedings and Collections (EPIC),
vol. 59,
pages 94-110,
EasyChair, 2019.
[ paper
| easychair
| bibtex
]
Armin Biere, Marijn Heule.
The Effect of Scrambling CNFs.
In Proc. 9th Work. on Pragmatics of SAT 2015 and 2018,
EasyChair Proceedings and Collections (EPIC),
vol. 59,
pages 111-126,
EasyChair, 2019.
[ paper
| bibtex
| scranfilize
]
Marijn Heule, Armin Biere.
What a Difference a Variable Makes.
In Proc. 24th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18),
Lecture Notes in Computer Science (LNCS),
vol. 10806,
pages 75-92,
Springer 2018.
[ paper
| bibtex
| experiments
]
Daniela Ritirc, Armin Biere, Manuel Kauers.
Improving and Extending the Algebraic Approach for Verifying Gate-Level Multipliers.
In Proc. Design, Automation and Test in Europe (DATE'18),
pages 1556-1561,
IEEE 2018.
[ paper
| bibtex
| experiments
]
Tom van Dijk, Rüdiger Ehlers, Armin Biere:
Revisiting Decision Diagrams for SAT.
CoRR abs/1805.03496 (2018)
[ paper
| arxiv
| bibtex
]
2017
Armin Biere, Manuel Kauers, Daniela Ritirc,.
Challenges in Verifying Arithmetic Circuits Using Computer Algebra.
In
Proc. 19th Intl. Symp. on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'17),
pages 9-15,
IEEE Computer Society, 2017.
[ paper
| bibtex
]
Best paper
Marijn Heule, Benjamin Kiesl, Martina Seidl, Armin Biere.
PRuning Through Satisfaction.
In Proc. 13th Haifa Verification Conference (HVC'17),
Lecture Notes in Computer Science (LNCS),
vol. 10629,
pages 179-194,
Springer 2017.
[ paper
| bibtex
| experiments
]
Best paper
Daniela Ritirc, Armin Biere, Manuel Kauers.
Column-Wise Verification of Multipliers Using Computer Algebra.
In Proc. 17th
Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'17),
pages 23-30,
IEEE 2017.
[ paper
| bibtex
| experiments
| pictures
]
Armin Biere, Tom van Dijk, Keijo Heljanko.
Hardware Model Checking Competition 2017.
In Proc. 17th
Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'17),
page 9,
IEEE 2017.
[ paper
| bibtex
| competition
]
Aina Niemetz, Mathias Preiner, Armin Biere.
Propagation based local search for bit-precise reasoning
.
In Journal of Formal Methods in System Design,
vol. 51(3),
pages 608-636,
Springer 2017.
[ paper
| preprint
| bibtex
| experiments
]
Armin Biere.
CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2017.
In Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions,
Tomas Tomáš, Marijn Heule, Matti Järvisalo (editors),
vol. B-2017-1 of Department of Computer Science Series of Publications B, pages 14-15, University of Helsinki, 2017.
[ paper
| bibtex
]
Armin Biere.
Deep Bound Hardware Model Checking Instances, Quadratic Propagation Benchmarks and Reencoded Factorization Problems Submitted to the SAT Competition 2017.
In Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions,
Tomas Tomáš, Marijn Heule, Matti Järvisalo (editors),
vol. B-2017-1 of Department of Computer Science Series of Publications B, pages 40-41, University of Helsinki, 2017.
[ paper
| bibtex
]
Aina Niemetz, Mathias Preiner, Armin Biere.
Model-Based API Testing for SMT Solvers.
In Proc. 15th Intl. Workshop on Satisfiability Modulo Theories (SMT'17),
10 pages, aff. to CAV'17, Heidelberg, Germany, 2017.
[ paper
| bibtex
| boolector
]
Best paper
Marijn Heule, Benjamin Kiesl, Armin Biere.
Short Proofs Without New Variables
.
In Proc. 26th Intl. Conf. on Automated Deduction (CADE'17).
Lecture Notes in Computer Science (LNCS),
vol. 10395,
pages 130-147,
Springer 2017.
[ paper
| bibtex
| experiments
]
Armin Biere, Steffen Hölldobler, Sibylle Möhle.
An Abstract Dual Propositional Model Counter.
In Proc. Young Scientist's Intl. Workshop on Trends in Information Processing (YSIP2'17),
vol. 1837 CEUR Workshop Proceedings,
pages 17-26, CEUR-WS.org 2017.
[ paper
| bibtex
]
Katalin Fazekas, Marijn J. H. Heule, Martina Seidl, Armin Biere.
Skolem Function Continuation for Quantified Boolean Formulas.
Proc. 11th Intl. Conf. on Tests and Proofs (TAP'17).
Lecture Notes in Computer Science vol. 10375, Springer, pages 129-138,
2017.
[ paper |
bibtex |
tool
]
Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere.
Blocked Clauses
in First-Order Logic.
Proc. 21st Intl. Conf. on Logic for Programming, Artificial
Intelligence and Reasoning (LPAR-21).
EasyChair Proceedings and Collections (EPIC),
vol. 46,
pages 31-48,
Easychair 2017.
[
preliminary extended version |
arxiv |
EasyChair |
bibtex ]
Mathias Preiner, Aina Niemetz, Armin Biere.
Counterexample-Guided Model Synthesis.
In Proc. 23rd Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17),
Lecture Notes in Computer Science (LNCS),
vol. 10205,
pages 264-280,
Springer 2017.
[ paper
| bibtex
| data
| boolector
]
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2017.
Technical Report 17/1, June 2017, FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[ report
| bibtex
| boolector
]
2016
Tomas Balyo,
Armin Biere,
Markus Iser,
Carsten Sinz.
SAT Race 2015,
in Journal of Artificial
Intelligence,
vol. 241,
pages 45-65,
Elsevier 2016.
[ preprint
| bibtex
| web
| ipasir.zip
| ipasir.h
]
Marijn Heule,
Armin Biere.
Clausal Proof Compression.
In Proc. 11th Intl. Workshop on the Implementation of Logics
(IWIL'15),
EasyChair Proceedings and Collections (EPIC),
vol. 40,
pages 21-26,
EasyChair, 2016.
[ paper
| bibtex
| ratz
| sbp
]
Akihisa Yamada,
Armin Biere,
Cyrille Artho,
Takashi Kitamura,
Eun-Hye Choi.
Greedy combinatorial test case generation using unsatisfiable cores
In Proc. 31st IEEE/ACM Intl. Conf. on Automated Software
Engineering (ASE'16),
pages 614-624,
ACM 2016.
[ paper
| bibtex
]
Aina Niemetz, Mathias Preiner, Armin Biere.
Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories.
In Proc. 28th Intl. Conf. on Computer Aided Verification (CAV'16),
Lecture Notes in Computer Science (LNCS),
vol. 9779,
pages 199-217,
Springer 2016.
[ paper
| bibtex
| data
| boolector
]
Armin Biere.
Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016.
In Proceedings of SAT Competition 2016 - Solver and Benchmark Descriptions,
Tomas Balyo, Marijn Heule, Matti Järvisalo (editors),
vol. B-2016-1 of Department of Computer Science Series of Publications B, pages 44-45, University of Helsinki, 2016.
[ paper
| bibtex
]
Armin Biere.
Collection of Combinational Arithmetic Miters Submitted to the SAT Competition 2016.
In Proceedings of SAT Competition 2016 - Solver and Benchmark Descriptions,
Tomas Balyo, Marijn Heule, Matti Järvisalo (editors),
vol. B-2016-1 of Department of Computer Science Series of Publications B, pages 65-66, University of Helsinki, 2016.
[ paper
| bibtex
| data
]
Aina Niemetz, Mathias Preiner,
Armin Biere.
Boolector at the SMT competition 2016.
Technical Report 16/1, June 2016, FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[ report
| bibtex
| boolector
]
2015
Florian Lonsing,
Fahiem Bacchus,
Armin Biere,
Uwe Egly, and
Martina Seidl.
Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination.
In Proc. 20th Intl. Conf. on Logic for Programming , Artificial Intelligence, and Reasoning 2015 (LPAR-20),
Lecture Notes in Computer Science (LNCS),
vol. 9450,
pages 418-433,
Springer 2015.
[ paper
[ bibtex
]
Marijn Heule, Armin Biere.
Compositional Propositional Proofs.
In Proc. 20th Intl. Conf. on Logic for Programming , Artificial Intelligence, and Reasoning 2015 (LPAR-20),
Lecture Notes in Computer Science (LNCS),
vol. 9450,
pages 444-459,
Springer 2015.
[ paper
| bibtex
| data
| drabt
]
Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly and Martina Seidl: Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. In Proc. 20th Intl. Conf. on Logic for Programming , Artificial Intelligence, and Reasoning 2015 (LPAR-20), Lecture Notes in Computer Science (LNCS), vol. 9450, pages 418-433, Springer 2015.
Mathias Preiner, Aina Niemetz, Armin Biere.
Better Lemmas with Lambda Extraction.
In Proc. 15th
Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'15),
pages 128-135,
FMCAD Inc. 2015.
[ paper
| bibtex
| boolector
]
Aina Niemetz, Mathias Preiner, Armin Biere, Andreas Fröhlich.
Improving
Local Search For Bit-Vector Logics in SMT with Path Propagation.
In Proc. 4th Intl. Work. on Design and Implementation of Formal Tools and Systems (DIFTS'15),
10 pages, aff. to FMCAD'15, Austin, TX, USA, 2015.
[ paper
| bibtex
| data
| boolector
]
Armin Biere, Andreas Fröhlich.
Evaluating CDCL Variable Scoring Schemes.
In Proc. 18th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'15),
Lecture Notes in Computer Science (LNCS),
vol. 9340,
pages 405-422,
Springer 2015.
[ paper
| bibtex
| data
]
Armin Biere, Andreas Fröhlich.
Evaluating CDCL Restart Schemes.
In Proc. Intl. Workshop on Pragmatics of SAT 2015 and 2018,
EasyChair Proceedings and Collections (EPIC),
vol. 59,
pages 1-17,
EasyChair, 2019.
[ paper
| bibtex
| data
]
Gergely Kovásznai, Andreas Fröhlich, Armin Biere.
Complexity of Fixed-Size Bit-Vector Logics (preprint).
Theory of Computing Systems (TOCS),
vol. 59, number 2,
pages 323-376,
Springer 2016,
first online Sept. 2015.
[ preprint
| bibtex
]
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector 2.0.
Journal of Satisfiability, Boolean Modeling and Computation (JSAT),
vol. 9,
pages 53-58,
2014 (published 2015),
IOS Press.
[ paper
| bibtex
| boolector
]
IJCAI-JAIR 2019 Award
Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, Armin Biere.
Clause Elimination for SAT and QSAT.
Journal of Artificial Intelligence Research (JAIR).
vol. 53,
pages 127-168,
2015.
[ link
| preprint
| bibtex
| lingeling
| bloqqer
| award
]
Marijn Heule, Martina Seidl, Armin Biere. Blocked Literals are Universal. In Proc. 7th Intl. Symp. NASA Formal Methods (NFM'15), Lecture Notes in Computer Science (LNCS), vol. 9058, pages 436 - 442, Springer 2015.
Akihisa Yamada, Takashi Kitamura, Cyrille Artho, Eun-Hye Choi, Yutaka Oiwa, Armin Biere. Optimization of Combinatorial Testing by Incremental SAT Solving. In Proc. 8th IEEE Intl. Conf. on Software Testing Verification, and Validation (ICST'15), pages 1 - 10, IEEE 2015.
Andreas Fröhlich, Armin Biere, Christoph Wintersteiger, Youssef Hamadi.
Stochastic Local Search for Satisfiability Modulo Theories.
In Proc. 29th AAAI Conf. on Artificial Intelligence (AAAI'15),
pages 1136 - 1143,
AAAI Press 2015.
[ paper
| bibtex
]
Marijn Heule, Armin Biere. Proofs for Satisfiability Problems. In All about Proofs, Proofs for All (APPA), Mathematical Logic and Foundations, vol. 55, pages 1 - 22, College Publications 2015.
Armin Biere.
Lingeling and Friends Entering the SAT Race 2015.
Technical Report 15/2, April 2015, FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[ report
| bibtex
| lingeling
]
Aina Niemetz, Mathias Preiner,
Armin Biere.
Boolector at the SMT Competition 2015.
Technical Report 15/1, June 2015, FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[ report
| bibtex
| boolector
]
2014
Gianpiero Cabodi, Carmelo Loiacono, Marco Palena, Paolo Pasini, Denis Patti, Stefano Quer,
Danilo Vendraminetto, Armin Biere, Keijo Heljanko.
Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks.
Journal of Satisfiability, Boolean Modeling and Computation (JSAT),
vol. 9,
pages 135-172,
IOS Press 2014.
[
paper |
bibtex
]
Gilles Audemard, Armin Biere, Jean-Marie Lagniez, Laurent Simon.
Améliorer SAT dans le cadre incrémental.
Revue d'Intelligence Artificielle,
593-614,
28(5),
2014.
[ paper ]
Marijn Heule, Martina Seidl, Armin Biere. Efficient Extraction of Skolem Functions from QRAT Proofs. In Proc. 14th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'14), 107-114, FMCAD Inc. 2014.
Aina Niemetz, Mathias Preiner, Armin Biere.
Turbo-Charging Lemmas on Demand with Don't Care
Reasoning.
In Proc. 14th
Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'14),
179-186,
FMCAD Inc 2014.
[ paper
| bibtex
| data
| boolector
]
Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov.
Experimenting with SAT Solvers in Vampire
.
In Proc. 13th Mexican Intl. Conf. on Artificial Intelligence (MICAI),
Lecture Notes in Computer Science (LNCS),
vol. 8856,
431-442,
Springer 2014.
[ paper
| bibtex
]
Gergely Kovásznai, Helmut Veith, Andreas Fröhlich, Armin Biere. On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic. In Proc. 39th Intl. Symp. on Mathematical Foundations of Computer Science (MFCS'14), Lecture Notes in Computer Science (LNCS), vol. 8635, 481-492, Springer 2014.
Armin Biere, Roderick Bloem (editors). Proc. 26th Intl. Conf. on Computer Aided Verification (CAV'14), Lecture Notes in Computer Science (LNCS), vol. 8559, Springer 2014.
Andreas Fröhlich, Gergely Kovásznai, Armin Biere, Helmut Veith. iDQ: Instantiation-Based DQBF Solving. In Proc. Intl. Workshop on Pragmatics of SAT (POS'14), EasyChair Proceedings and Collections (EPIC), vol. 27, 103-116, EasyChair 2014.
Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov.
SAT solving experiments in Vampire
.
In Proc. 1st and 2nd Vampire Workshop (Vampire'14 and Vampire'15),
EasyChair Proceedings and Collections (EPIC),
vol. 38,
29-32,
EasyChair 2016.
[ paper
| bibtex
]
Armin Biere.
Yet another Local Search Solver and Lingeling and Friends Entering the SAT Competition 2014.
In Proceedings of SAT Competition 2014,
Adrian Balint, Anton Belov, Marijn Heule, Matti Järvisalo (editors),
vol. B-2014-2 of Department of Computer Science Series of Publications B, pages 39-40, University of Helsinki, 2014.
[ paper
| bibtex
]
Marijn Heule, Martina Seidl, Armin Biere. A Unified Proof System for QBF Preprocessing, In Proc. 7th Joint Conf. on Automated Reasoning (IJCAR'14), Lecture Notes in Computer Science (LNCS), vol. 8562, 91-106, Springer 2014.
Adrian Balint, Armin Biere, Andreas Fröhlich, Uwe Schöning. Improving implementation of SLS solvers for SAT and new heuristics for k-SAT with long clauses. In Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Lecture Notes in Computer Science (LNCS), vol. 8561, 302-316, Springer 2014.
Tomas Balyo, Andreas Fröhlich, Marijn Heule, Armin Biere. Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask). In Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Lecture Notes in Computer Science (LNCS), vol. 8561, 317-332, Springer 2014.
Armin Biere, Daniel Le Berre, Emmanuel Lonca, Norbert Manthey. Detecting cardinality constraints in CNF. In Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Lecture Notes in Computer Science (LNCS), vol. 8561, 285-301, Springer 2014.
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2014.
Technical Report 14/1, June 2014, FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[ report
| bibtex
| boolector
]
2013
Marijn Heule, Armin Biere. Blocked Clause Decomposition. In Proc. 19th Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning 2013 (LPAR-19), Lecture Notes in Computer Science (LNCS), vol. 8312, pages 423–438, Springer 2013.
Cyrille Artho, Armin Biere, Masami Hagiya, Eric Platon, Martina Seidl, Yoshinori Tanabe, Mitsuharu Yamamoto. Modbat: A Model-based API Tester for Event-driven Systems. In Proc. Haifa Verification Conference (HVC'13), Lecture Notes in Computer Science (LNCS), vol. 8244, pages 112-128, Springer 2013.
Mathias Preiner, Aina Niemetz, Armin Biere.
Lemmas on Demand for Lambdas.
In Proc. 2nd Intl. Work. on Design and Implementation of Formal Tools and Systems (DIFTS'13),
10 pages, aff. to FMCAD'13, Portland, Oregon, USA, 2013.
[ paper
| bibtex
| data
| boolector
]
Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr. SmacC: A Retargetable Symbolic Execution Engine. In Proc. 11th Intl. Symp. on Automated Technology for Verification and Analysis (ATVA'13), Lecture Notes in Computer Science (LNCS), vol. 8172, pages 482-486, Springer 2013.
Andreas Fröhlich, Gergely Kovásznai, Armin Biere. Efficiently Solving Bit-Vector Problems Using Model Checkers. In Proc. 11th Intl. Workshop on Satisfiability Modulo Theories (SMT'13), pages 6-15, aff. to SAT'13, Helsinki, Finland, 2013.
Aina Niemetz, Armin Biere.
ddSMT: A Delta Debugger for the SMT-LIB v2 Format.
In Proc. 11th Intl. Workshop on Satisfiability Modulo Theories (SMT'13),
pages 36-45, aff. to SAT'13, Helsinki, Finland, 2013.
[ paper
| bibtex
| ddsmt
]
Martin Aigner, Armin Biere, Christoph Kirsch, Aina Niemetz, Mathias Preiner. Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures. In Proc. Intl. Workshop on Pragmatics of SAT (POS'13), EasyChair Proceedings and Collections (EPIC), vol. 29, 28-40, EasyChair 2014.
Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr. The Auspicious Couple: Symbolic Execution and WCET Analysis. In Proc. 13th Intl. Work. on Worst-Case Execution Time Analysis (WCET'13), OASICS series, vol. 30, pages 53-63, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013.
Armin Biere. Lingeling, Plingeling and Treengeling Entering the SAT Competition 2013. In Proceedings of SAT Competition 2013, Adrian Balint, Anton Belov, Marijn Heule, Matti Järvisalo (editors), vol. B-2013-1 of Department of Computer Science Series of Publications B, pages 51-52, University of Helsinki, 2013.
Armin Biere. Two Pigeons per Hole Problem. In Proceedings of SAT Competition 2013, Adrian Balint, Anton Belov, Marijn Heule, Matti Järvisalo (editors), vol. B-2013-1 of Department of Computer Science Series of Publications B, page 103, University of Helsinki, 2013.
Armin Biere, Marijn Heule, Matti Järvisalo, Norbert Manthey.
Equivalence checking of HWMCC 2012 Circuits.
In Proceedings of SAT Competition 2013,
Adrian Balint, Anton Belov, Marijn Heule, Matti Järvisalo (editors),
vol. B-2013-1 of Department of Computer Science Series of Publications B, page 104 , University of Helsinki, 2013.
[ paper
| bibtex
| hwmcc12
| miters
| aiger
]
Gergely Kovásznai, Andreas Fröhlich, Armin Biere. Quantifier-Free Bit-Vector Formulas with Binary Encoding: Benchmark Description. In Proceedings of SAT Competition 2013, Adrian Balint, Anton Belov, Marijn Heule, Matti Järvisalo (editors), vol. B-2013-1 of Department of Computer Science Series of Publications B, pages 107-108 , University of Helsinki, 2013.
Jean-Marie Lagniez, Armin Biere. Factoring Out Assumptions to Speed Up MUS Extraction. In Proc. 16th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'13), Lecture Notes in Computer Science (LNCS), vol. 7962, pages 276-292, Springer 2013.
Gergely Kovásznai, Andreas Fröhlich, Armin Biere. BV2EPR: A Tool for Polynomially Translating Quantifier-free Bit-Vector Formulas into EPR. In Proc. 24th Intl. Conf. on Automated Deduction (CADE'13), Lecture Notes in Computer Science (LNCS), vol. 7898, pages 443-449, Springer 2013.
Andreas Fröhlich, Gergely Kovásznai, Armin Biere. More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding. In Proc. 8th Intl. Computer Science Symp. in Russia (CSR'13), Lecture Notes in Computer Science (LNCS), vol. 7913, pages 378-390, Springer 2013 (with appendix).
Cyrille Artho, Armin Biere, Martina Seidl. Model-Based Testing for Verification Backends. In Proc. 7th Intl. Conf. on Tests & Proofs (TAP'13), Lecture Notes in Computer Science (LNCS), vol. 7942, pages 39-55, Springer 2013.
Marijn Heule, Matti Järvisalo, Armin Biere. Revisiting Hyper Binary Resolution. In Proc. 10th Intl. Conf. on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'13), Lecture Notes in Computer Science (LNCS), vol. 7874, pages 77-93, Springer 2013.
Alexandra Goultiaeva, Martina Seidl, Armin Biere. Bridging the Gap between Dual Propagation and CNF-based QBF Solving. In Proc. Intl. Conf. on Design, Automation & Test in Europe (DATE'13), pages 811-814, 2013.
2012
Cyrille Artho, Armin Biere, Masami Hagiya, Richard Potter, Rudolf Ramler, Yoshinori Tanabe, Franz Weitl, Mitusharu Yamamoto. Modbat: A model-based API tester for event-driven systems. Short paper (tool demo) at the Dependable Systems Workshop 2012, 2 pages, Kobe, Japan, December 2012.
Norbert Manthey, Marijn Heule, Armin Biere. Automated Reencoding of Boolean Formulas. In Proc. Haifa Verification Conference (HVC'12), Lecture Notes in Computer Science (LNCS), vol. 7857, pages 102-117, Springer 2013.
Magdalena Widl, Armin Biere, Petra Brosch, Uwe Egly, Marijn Heule, Gerti Kappel, Martina Seidl, Hans Tompits. Guided Merging of Sequence Diagrams. In revised selected papers of 5th Intl. Conf. on Software Language Engineering (SLE'12), Lecture Notes in Computer Science (LNCS), vol. 7745 pages 164-183, Springer 2012.
Matti Järvisalo, Armin Biere, Marijn Heule. Simulating Circuit-Level Simplifications on CNF. Journal of Automated Reasoning, 49(4), pages 583-619, Springer 2012.
Alexander Nöhrer, Armin Biere, Alexander Egyed. A comparison of strategies for tolerating inconsistencies during decision-making. In Proc. 16th Intl. Software Product Line Conf. (SPLC'12), pages 11-20, ACM, 2012.
Gergely Kovásznai, Andreas Fröhlich, Armin Biere. On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width. In Proc. 10th Intl. Workshop on Satisfiability Modulo Theories (SMT'12), EasyChair Proceedings and Collections (EPIC), vol. 20, pages 44-56, EasyChair 2013.
Martina Seidl, Florian Lonsing, Armin Biere. QBF2EPR: A Tool for Generating EPR Formulas from QBF In Proc. 3rd Intl. Workshop. on Practical Aspects of Automated Reasoning (PAAR'12), EasyChair Proceedings and Collections (EPIC), vol. 21, pages 139-148, EasyChair 2013.
Vladimir Klebanov, Bernhard Beckert, Armin Biere, Geoff Sutcliffe (editors), Proc. 1st Intl. Work. on Comparative Empirical Evaluation of Reasoning Systems (COMPARE'12), vol. 873, CEUR Workshop Proceedings.
Armin Biere.
Lingeling and Friends Entering the SAT Challenge 2012.
In Proc. of SAT Challenge 2012: Solver and Benchmark Descriptions,
Adrian Balint, Anton Belov, Daniel Diepold, Simon Gerber, Matti Järvisalo, and Carsten Sinz (editors),
vol. B-2012-2 of Department of Computer Science Series of Publications B, pages 33-34, University of Helsinki, 2012.
[ paper
| bibtex
]
Peter van der Tak, Marijn Heule, and Armin Biere. Concurrent Cube-and-Conquer. In Proc. of SAT Challenge 2012: Solver and Benchmark Descriptions, Adrian Balint, Anton Belov, Daniel Diepold, Simon Gerber, Matti Järvisalo, and Carsten Sinz (editors), vol. B-2012-2 of Department of Computer Science Series of Publications B, pages 15-16, University of Helsinki, 2012.
Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere.
Resolution-Based Certificate Extraction for QBF (Tool Presentation).
In Proc. 15th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'12),
Lecture Notes in Computer Science (LNCS),
vol. 7317,
pages 430-435,
Springer 2012.
[ paper
| bibtex
| qbfcert
]
Peter van der Tak, Marijn Heule, Armin Biere. Concurrent Cube-and-Conquer (Poster Presentation). In Proc. 15th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'12), Lecture Notes in Computer Science (LNCS), vol. 7317, pages 475-476, Springer 2012.
Andreas Fröhlich, Gergely Kovásznai, Armin Biere. A DPLL Algorithm for Solving DQBF. In Proc. Intl. Workshop on Pragmatics of SAT (POS'12), aff. to SAT'12, Trento, Italy, 2012.
Peter van der Tak, Marijn Heule, Armin Biere. Concurrent Cube-and-Conquer. In Proc. Intl. Workshop on Pragmatics of SAT (POS'12), aff. to SAT'12, Trento, Italy, 2012.
Matti Järvisalo, Marijn Heule, Armin Biere. Inprocessing Rules. In Bernhard Gramlich, Dale Miller, and Uli Sattler (editors), Proc. 6th Intl. Joint Conf. on Automated Reasoning (IJCAR'12), Lecture Notes in Computer Science (LNCS), vol. 7364, pages 355-370, Springer 2012.
Alexander Nöhrer, Armin Biere, Alexander Egyed. Managing SAT Inconsistencies with HUMUS. In Proc. 6th Intl. Workshop on Variability Modelling of Software-Intensive Systems (VaMoS'12), pages 83-91, ACM 2012.
Armin Biere.
Boolector Entering the SMT Competition 2012.
Technical Report 12/1, June 2012, FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[ report
| bibtex
| boolector
]
2011
Armin Biere, Keijo Heljanko, Siert Wieringa.
AIGER 1.9 And Beyond,
Technical Report 11/2, July 2011, FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[ report
| bibtex
| github
| aiger
]
Best paper
Marijn Heule, Oliver Kullmann, Siert Wieringa,
Armin Biere.
Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads.
In Proc. 7th Intl. Haifa Verification Conference (HVC'11),
Lecture Notes in Computer Science (LNCS),
vol. 7261,
pages 50-65,
Springer 2012 (software).
Malay Ganai, Armin Biere (editors). Proc. 1st Intl. Workshop on Design and Implementation of Formal Tools and Systems (DIFTS'11), vol. 832, CEUR Workshop Proceedings. Aff. workshop to FMCAD'2011, Austin, Texas, USA, Nov. 2011.
Armin Biere, Karen Yorav. Preface Special Issue on Hardware Verification Workshop (HWVW'10). Formal Methods in System Design, vol. 39, number 2, pages 115-116, Springer 2011.
Armin Biere, Florian Lonsing, Martina Seidl. Blocked Clause Elimination for QBF. In Proc. 23rd Intl. Conf. on Automated Deduction (CADE'11), Lecture Notes in Computer Science (LNCS), vol. 6803, pages 101-115, Springer 2011.
Marijn Heule, Matti Järvisalo, Armin Biere. Efficient CNF Simplification Based on Binary Implication Graphs. In Proc. 14th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'11), Lecture Notes in Computer Science (LNCS), vol. 6695, pages 201-215, Springer 2011.
Florian Lonsing, Armin Biere. Failed Literal Detection for QBF. In Proc. 14th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'11), Lecture Notes in Computer Science (LNCS), vol. 6695, pages 259-272, Springer 2011.
Armin Biere.
Boolector Entering the SMT Competition 2011.
Technical Report 11/3, June 2011, FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[ report
| bibtex
| boolector
]
Armin Biere.
Lingeling and Friends at the SAT Competition 2011.
Technical Report 11/1, March 2011, FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[ report
| bibtex
]
2010
Marijn Heule, Matti Järvisalo, Armin Biere. Covered Clause Elimination. In Short Paper Proc. 17th Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning 2010 (LPAR-17), EasyChair Proceedings and Collections (EPIC), vol. 13, pages 41-46, EasyChair 2013.
Marijn Heule, Matti Järvisalo, Armin Biere. Clause Elimination Procedures for CNF Formulas. In Proc. 17th Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning 2010 (LPAR-17), Lecture Notes in Computer Science (LNCS), vol. 6397, pages 357–371, Springer 2010.
Florian Lonsing, Armin Biere. Integrating Dependency Schemes in Search-Based QBF Solvers. In Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10), Lecture Notes in Computer Science (LNCS), vol. 6175, pages 158-171, Springer 2010. (ERRATA).
Matti Järvisalo, Armin Biere. Reconstructing Solutions after Blocked Clause Elimination. In Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10), Lecture Notes in Computer Science (LNCS), vol. 6175, pages 340-345, Springer 2010.
Robert Brummayer, Florian Lonsing, Armin Biere. Automated Testing and Debugging of SAT and QBF Solvers. In Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10), Lecture Notes in Computer Science (LNCS), vol. 6175, pages 44-57, Springer 2010. [ paper | bibtex | qbfuzz | qbfdd ]
Armin Biere. Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical Report 10/1, August 2010, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria.
Florian Lonsing, Armin Biere. DepQBF: A Dependency-Aware QBF Solver (System Description). Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 7, 2010, pages 71-76.. Preliminary version appeared in Proc. 1st Intl. Work. on Pragmatics of SAT (POS'10).
Matti Järvisalo, Armin Biere, Marijn Heule. Blocked Clause Elimination. In Proc. 16th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10), Lecture Notes in Computer Science (LNCS), vol. 6015, pages 129-144, Springer 2010.
2009
Armin Biere, Carl Pixley (editors). Proceedings 9th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'09), IEEE 2009.
Robert Brummayer, Armin Biere. Fuzzing and Delta-Debugging SMT Solvers. In Proc. 7th Intl. Workshop on Satisfiability Modulo Theories (SMT'09), 5 pages, ACM 2009.
Niklas Sörensson, Armin Biere. Minimizing Learned Clauses. In Proc. 12th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'09), Lecture Notes in Computer Science (LNCS), vol. 5584, pages 237-243, Springer 2009.
Florian Lonsing, Armin Biere. A Compact Representation for Syntactic Dependencies in QBFs. In Proc. 12th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'09), Lecture Notes in Computer Science (LNCS), vol. 5584, pages 398-411, Springer 2009.
Robert Brummayer, Armin Biere.
Lemmas on Demand for the Extensional Theory of Arrays.
Journal on Satisfiability, Boolean Modeling and Computation (JSAT),
vol. 6,
pages 165-201,
Delft University, 2009.
[ paper
| bibtex
| boolector
]
Robert Brummayer, Armin Biere.
Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays.
In Proc. 15th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'09),
Lecture Notes in Computer Science (LNCS),
vol. 5505,
pages 174-177,
Springer 2009.
[ paper
| bibtex
| boolector
]
Armin Biere.
P{re,i}coSAT@SC'09.
Solver description for SAT Competition 2009.
In SAT 2009 Competitive Event Booklet, 2009.
[ paper
| bibtex
]
Robert Brummayer, Armin Biere. Effective Bit-Width and Under-Approximation. In Proc. 12th Intl. Conference on Computer Aided Systems Theory (EUROCAST'09), Lecture Notes in Computer Science (LNCS), vol. 5717, pages 304-311 Springer 2009.
Armin Biere. Bounded Model Checking. In Handbook of Satisfiability. IOS Press, February 2009, pages 455-481. See also this link.
Armin Biere, Marijn Heule, Hans Van Maaren and Toby Walsh (editors). Handbook of Satisfiability. IOS Press, February 2009.
2008
Armin Biere, Robert Brummayer. Consistency Checking of All Different Constraints over Bit-Vectors within a SAT-Solver. In Proc. 8th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'08), IEEE 2008.
Florian Lonsing, Armin Biere. Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers. In Selected Papers of Proc. 4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'08), Znojmo, Czech Republic, November 2008. Appeared in ENTCS, vol. 251, pages 83-95, Elsevier 2009. (DOI) (Preprint) (Preliminary version)
Armin Biere. Tutorial on Model Checking, Modelling and Verification in Computer Science. In Proc. 3rd Intl. Conf. on Algebraic Biology (AB'08), Lecture Notes in Computer Science (LNCS), vol. 5147, Springer 2008.
Best student paper
Robert Brummayer, Armin Biere, Florian Lonsing.
BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking.
In Proc. 1st Intl. Workshop on Bit-Precise Reasoning (BPR'08), Princeton, New Jersey, USA, July 2008.
[ paper
| bibtex
]
Robert Brummayer, Armin Biere.
Lemmas on Demand for the Extensional Theory of Arrays.
In Proc. 6th Intl. Workshop on Satisfiability Modulo Theories (SMT'08), Princeton, New Jersey, USA, July 2008.
[ paper
| bibtex
| boolector
]
Florian Lonsing, Armin Biere. Nenofex: Expanding NNF for QBF Solving. In Proc. 11th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'08), Lecture Notes in Computer Science (LNCS), vol. 4996, Springer 2008.
Armin Biere. Adaptive Restart Control for Conflict Driven SAT Solvers. In Proc. 11th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'08), Lecture Notes in Computer Science (LNCS), vol. 4996, Springer 2008.
Armin Biere, Daniel Kröning, Georg Weissenbacher, Christoph Wintersteiger. Digitaltechnik - Eine praxisnahe Einführung. Springer 2008.
2007
Armin Biere.
The AIGER And-Inverter Graph (AIG) Format Version 20071012.
Technical Report 07/1, October 2011, FMV Reports Series,
Institute for Formal Models and Verification,
Johannes Kepler University,
Altenbergerstr. 69, 4040 Linz, Austria.
[ report
| bibtex
| github
| aiger
]
Robert Brummayer, Armin Biere. C32SAT: Checking C Expressions. In Proc. 19th Intl. Conf. on Computer Aided Verification (CAV'07), Lecture Notes in Computer Science (LNCS), vol. 4590, Springer 2007.
Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kröning, Christoph Wintersteiger. A First Step Towards a Unified Proof Checker for QBF. In Proc. 10th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'07), Lecture Notes in Computer Science (LNCS), vol. 4501, Springer 2007.
Cyrille Artho, Boris Zweimüller, Armin Biere, Etsuya Shibayama, Shinichi Honiden. Efficient Model Checking of Applications with Input/Output. In Proc. Computer Aided Systems Theory (EUROCAST'07), Lecture Notes in Computer Science (LNCS), vol. 4739, Springer 2007.
2006
Armin Biere, Keijo Heljanko, Tommi Junttila, Timo Latvala, Viktor Schuppan. Linear Encodings of Bounded LTL Model Checking. Logical Methods in Computer Science, vol. 2, issue 5:5, 2006, 10.2168/LMCS-2(5:5)2006.
Robert Brummayer, Armin Biere. Local Two-Level And-Inverter Graph Minimization without Blowup. In Proc. 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'06), Mikulov, Czechia, October 2006.
Ofer Strichman, Armin Biere (editors). Proc. 4th Intl. Workshop on Bounded Model Checking (BMC'06), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 174, issue 3, Elsevier 2007.
Toni Jussila, Armin Biere. Compressing BMC Encodings with QBF. In Proc. 4th Intl. Workshop on Bounded Model Checking (BMC'06), to be published in Electronic Notes in Theoretical Computer Science (ENTCS), Seattle, USA, August 2006.
Armin Biere, Carla Gomes (editors). Proc. 9th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'06), Lecture Notes in Computer Science (LNCS), vol. 4121, Springer 2006, 10.1007/11814948.
Toni Jussila, Carsten Sinz, Armin Biere. Extended Resolution Proofs for Symbolic SAT Solving with Quantification. In Proc. 9th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'06), Lecture Notes in Computer Science (LNCS), vol. 4121, Springer 2006.
Cyrille Artho, Armin Biere, Shinichi Honiden. Enforcer - Efficient Failure Injection. In Proc. Formal Methods (FM'06), Lecture Notes in Computer Science (LNCS), vol. 4085, Springer 2006, 10.1007/11813040_28.
Cyrille Artho, Armin Biere, Shinichi Honiden, Viktor Schuppan, Pascal Eugster, Marcel Baur, Boris Zweimüller, Peter Farkas. Advanced Unit Testing - How to Scale Up a Unit Test Framework. In Proc. Workshop on Automation of Software Test (AST'06), Shanghai, China, May 2006.
Carsten Sinz, Armin Biere. Extended Resolution Proofs for Conjoining BDDs. In Proc. 1st Intl. Computer Science Symp. in Russia (CSR 2006), St. Petersburg, Russia, Lecture Notes in Computer Science (LNCS), vol. 3967, Springer 2006.
Armin Biere, Carsten Sinz. Decomposing SAT Problems into Connected Components. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 2, Delft University, 2006.
Armin Biere. (Q)CompSAT and (Q)PicoSAT at the SAT’06 Race. SAT Race 2006 Solver Description, 2006.
2005
Viktor Schuppan, Armin Biere. Liveness Checking as Safety Checking for Infinite State Spaces. Proc. 7th Intl. Workshop on Verification of Infinite-State Systems (INFINITY'05), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 149, issue 1, Elsevier 2006.
Armin Biere, O. Strichman (editors). Proc. 3rd Intl. Workshop on Bounded Model Checking (BMC'05). Electronic Notes in Theoretical Computer Science (ENTCS), vol. 144, issue 1, Elsevier 2006.
Niklas Eén, Armin Biere. Effective Preprocessing in SAT through Variable and Clause Elimination. In Proc. 8th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'05), Lecture Notes in Computer Science (LNCS), vol. 3569, Springer 2005, 10.1007/11499107_5.
Malek Haroud, Armin Biere. SDL versus C Equivalence Checking. In Proc. 12th SDL Forum (SDL'05), Lecture Notes in Computer Science (LNCS), vol. 3530, Springer 2005.
Cyrille Artho, Armin Biere. Subroutine Inlining and Bytecode Abstraction to Simplify Static and Dynamic Analysis. In Proc. 1st Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'05), Edinburgh, Scotland, UK, April 2005, Electronic Notes in Theoretical Computer Science (ENTCS), vol. 141, issue 1, Elsevier 2006.
Viktor Schuppan, Armin Biere. Shortest Counterexamples for Symbolic Model Checking of LTL with Past. In Proc. 11th Intl. Conf. on Tools and Algorithms for the Analysis and Construction of Systems (TACAS'05), Lecture Notes in Computer Science (LNCS), vol. 3440, Springer 2005, ext. version available as ETH Technical Report 470.
Mukul Prasad, Armin Biere, Aarti Gupta. A Survey of Recent Advances in SAT-based Formal Verification, Intl. Journal on Software Tools for Technology Transfer (STTT), vol. 7, number 2, Springer 2005.
Viktor Schuppan, Armin Biere. Shortest Counterexamples for Symbolic Model Checking of LTL with Past. Technical Report 470, Dept. of Computer Science, ETH Zürich, 2005, full version of our TACAS'05 paper.
Cyrille Artho, Armin Biere. Combined Static and Dynamic Analysis. Technical Report 466, Dept. of Computer Science, ETH Zürich, 2005, full version of our AIOOL'05 paper.
Cyrille Artho, Armin Biere. Combined Static and Dynamic Analysis. In Proc. 1st Intl. Workshop on Abstract Interpretation of Object-Oriented Languages (AIOOL'05), Paris, France, Jan. 2005, ext. version available as ETH Technical Report 466.
Timo Latvala, Armin Biere, Keijo Heljanko, Tommi Junttila. Simple is Better: Efficient Bounded Model Checking for Past LTL. In Proc. 6th Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI'05), Paris, France, Jan. 2005, Lecture Notes in Computer Science (LNCS), vol. 3385, Springer 2005.
2004
Cyrille Artho, Klaus Havelund, Armin Biere. Using Block-local Atomicity to Detect Stale-value Concurrency Errors. In Proc. 2nd Intl. Symp. on Automated Technology for Verification and Analysis (ATVA'04), Taipei, Nov. 2004, Lecture Notes in Computer Science (LNCS), vol. 3299, Springer 2004.
Timo Latvala, Armin Biere, Keijo Heljanko, Tommi Junttila. Simple Bounded LTL Model Checking. In Proc. Formal Methods in Computer-Aided Design (FMCAD'04), Austin Texas, Nov. 2004, Lecture Notes in Computer Science (LNCS), vol. 3312, Springer 2004.
Malek Haroud, Ljubica Blažević, Armin Biere. HW accelerated ultra wide band MAC protocol using SDL and SystemC. In Proc. IEEE Radio and Wireless Conference (RAWCON'04), IEEE, Sept. 2004.
Timo Latvala, Armin Biere, Keijo Heljanko, Tommi Junttila. Simple bounded LTL model checking. Research Report A92, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, July 2004.
Armin Biere, Ofer Strichman (editors). Proc. 2nd Intl. Workshop on Bounded Model Checking (BMC'04). Electronic Notes in Theoretical Computer Science (ENTCS), vol. 119, issue 2, Elsevier 2005.
Cyrille Artho, Viktor Schuppan, Armin Biere, Pascal Eugster, Marcel Baur, Boris Zweimüller. JNuke: Efficient Dynamic Analysis for Java. In Proc. 16th Intl. Conf. on Computer-Aided Verification (CAV'04), Lecture Notes in Computer Science (LNCS), vol. 3114, Springer 2004.
Test-of-time award SAT'23
Armin Biere.
Resolve and Expand.
In Proc. 7th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'04),
Lecture Notes in Computer Science (LNCS),
vol. 3542,
Springer 2005,
10.1007/11527695_5.
[ paper
| bibtex
| quantor
| award
]
Armin Biere. The Evolution from Limmat to Nanosat. Technical Report 444, Dept. of Computer Science, ETH Zürich 2004.
Viktor Schuppan, Marcel Baur, Armin Biere. VM Independent Replay in Java. In Proc. 4th Intl. Workshop on Runtime Verification (RV'04), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 113, Elsevier 2005.
Viktor Schuppan, Armin Biere. Efficient reduction of finite state model checking to reachability analysis. Intl. Journal on Software Tools for Technology Transfer (STTT), vol. 5, number 2-3, Springer 2004.
2003
Cyrille Artho, Klaus Havelund, Armin Biere. High-Level Data Races. Software Testing, Verification & Reliability (STVR), vol. 13, number 4, John Wiley & Sons 2003.
Viktor Schuppan, Armin Biere. Verifying the IEEE 1395 FireWire Tree Identify Protocol with SMV. Formal Aspects of Computing, vol. 14, number 3, Springer 2003.
David Plaisted, Armin Biere, Yunshan Zhu. A Satisfiability Tester for Quantified Boolean Formulae. Discrete Applied Mathematics (DAM), vol. 130, number 2, Elsevier 2003.
Cyrille Artho, Klaus Havelund, Armin Biere. High-Level Data Races. In Proc. 1st Intl. Workshop on Verification and Validation of Enterprise Information Systems (VVEIS'03), Angers, France, ICEIS Press 2003.
Armin Biere, Alessandro Cimatti, Edmund Clarke, Ofer Strichman, Yunshan Zhu. Bounded Model Checking. In Advances in Computers, vol. 58, Academic Press 2003.
Armin Biere, Ofer Strichman (editors). Proc. 1st Intl. Workshop on Bounded Model Checking (BMC'03), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 89, issue 4, Elsevier 2004.
2002
Armin Biere, Wolfgang Kunz. SAT and ATPG: Boolean Engines for Formal Hardware Verification. In Proc. IEEE/ACM Intl. on Computer Aided Design (ICCAD'02), Nov. 2002.
Armin Biere, Cyrille Artho, Viktor Schuppan. Liveness Checking as Safety Checking. In Proc. 7th Intl. Workshop on Formal Methods for Industrial Critical Systems (FMICS'02), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 66, number 2, Elsevier 2002.
Sergey Berezin, Edmund Clarke, Armin Biere, Yunshan Zhu. Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function. Formal Methods in System Design (FMSD), vol. 20, number 2, Kluwer 2002.
2001
Armin Biere. Verifying Sequential Behavior with Model Checking. In Proc. 4th Intl. Conf. on ASIC (ASICON'01), Shanghai, China, IEEE Press and People's Posts & Telecommunications Publishing Office 2001
Edmund Clarke, Armin Biere, Richard Raimi, Yunshan Zhu. Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design (FMSD), vol. 19, number 1, Kluwer 2001.
Cyrille Artho, Armin Biere. Applying Static Analysis to Large-scale, Multi-threaded Java Programs. In Proc. Australian Software Engineering Conf. (ASWEC'01), IEEE 2001, got most influential paper award in 2013.
Viktor Schuppan, Armin Biere. A Simple Verification of the Tree Identify Protocol with SMV. In Proc. IEEE 1394 (FireWire) Workshop, Technical Report Dept. of Computing Science and Mathematics, Univ. of Stirling, March 2001.
2000
Poul Williams, Armin Biere, Edmund Clarke, Aarti Gupta. Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. In Proc. Intl. Conf. on Computer-Aided Verification (CAV'00), Lecture Notes in Computer Science (LNCS), vol. 1855, Springer 2000, 10.1007/10722167_13.
1999
Armin Biere, Edmund Clarke, Yunshan Zhu. Multiple State and Single State Tableaux for Combining Local and Global Model Checking. In E.-R. Olderog, B. Steffen (Eds.), Correct System Design Recent Insights and Advances, special issue dedicated to Hans Langmaack, Lecture Notes in Computer Science (LNCS), vol. 1710, Springer 1999, ext. version of our SMC'99 paper.
Armin Biere, Alessandro Cimatti, Edmund Clarke, Masahiro Fujita, Yunshan Zhu. Symbolic Model Checking using SAT procedures instead of BDDs. In Proc. ACM Design Automation Conf. (DAC'99), ACM 1999.
Armin Biere, Edmund Clarke, Richard Raimi, Yunshan Zhu. Verifying Safety Properties of a PowerPC™ Microprocessor Using Symbolic Model Checking without BDDs. In Proc. Intl. Conf. on Computer-Aided Verification (CAV'99), Lecture Notes in Computer Science (LNCS), vol. 1633, Springer 1999.
Armin Biere, Alessandro Cimatti, Edmund Clarke, Yunshan Zhu.
Symbolic Model Checking without BDDs.
In Proc. Intl. Conf. on Tools and Algorithms for the Analysis and Construction of Systems (TACAS'99),
Lecture Notes in Computer Science (LNCS),
vol. 1579,
Springer 1999.
[ paper
| bibtex
]
Armin Biere, Edmund Clarke, Yunshan Zhu. Combining Local and Global Model Checking. In Proc. 1st Intl. Workshop on Symbolic Model Checking (SMC'99), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 23, number 2, Elsevier 1999, long version.
1998
Sergey Berezin, Armin Biere, Edmund Clarke, Yunshan Zhu. Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. In Proc. Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'98), Lecture Notes in Computer Science (LNCS), vol. 1522, Springer 1998.
Bwolen Yang, Randal Bryant, David O'Hallaron, Armin Biere, Olivier Coudert, Geert Janssen, Rajeev Ranjan, Fabio Somenzi. A Performance Study of BDD-based Model Checking. In Proc. Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'98), Lecture Notes in Computer Science (LNCS), vol. 1522, Springer 1998.
1997
Armin Biere. mu-cke - Efficient mu-Calculus Model Checking. In Proc. Intl. Conf. on Computer-Aided Verification (CAV'97), Lecture Notes in Computer Science (LNCS), vol. 1254, Springer 1997.
Armin Biere. Efficient Model Checking of the Mu-Calculus with Binary Decision Diagrams. Ph.D. Thesis Univ. of Karlsruhe, Germany, Jan. 1997 (in German only).
1993
Armin Biere. Normalisation, Unification and Generalisation in Free Monoids. Diploma Thesis Univ. of Karlsruhe, Germany, Sept. 1993 (in German only).
Talks
2020 ]
2021 |
2022 |
2023 |
2024
2010 ]
2011 |
2012 |
2013 |
2014 |
2015 |
2016 |
2017 |
2018 |
2019
2000 |
2001 |
2002 |
2003 ]
2004 |
2005 |
2006 |
2007 |
2008 |
2009
Talks 2024
Dynamic Blocked Clause Elimination for Projected Model Counting
27th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'24)
Pune, India, August 23, 2024
[ slides
| paper
]
27th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'24)
Pune, India, August 21, 2024
[ slides | paper ] Advanced SAT Tutorial
Quantum Leaps and Local Search
SAT + SMT Summer School 2024
Pune, India, August 19, 2024
[ slides | exercise ]
Acceptance speech
Herbrand Award Talk
13th Intl. Joint Conf. on Automated Reasoning (IJCAR'24)
Nancy, France, July 4, 2024
[ slides
| award
]
Advanced SAT
SAT/SMT/AR Summer School 2024
Nancy, France, June 26, 2024
[ slides ]
Invited talk
30 Years of Faster and Faster SAT Solving
25th Intl. Conf. on Logic for
Programming, Artificial Intelligence and Reasoning (LPAR'24)
Mauritius, May 27, 2024
[ 30 Years of Faster and Faster SAT Solving
| SAT Museum
]
Talks 2023
The Art of Igniting the SAT Revolution
Shonan Seminar The Art of SAT
Shonan Village Center, Japan, October 2, 2023
[
slides |
program
]
The SAT Museum
14th International Workshop on Pragmatics of SAT (POS'23)
Alghero, Italy, July 4, 2023
[
slides
]
Talks 2022
Keynote
Fueling the SAT Revolution in Automated Reasoning
50 Jahre KIT-Fakultät für Informatik
Karlsruhe, October 20, 2022
[
slides |
pictures
]
SAT Solving
Hausdorff School for Advanced Studies in Mathematics
Computational Combinatorial Optimization
Bonn, September 12 - 16, 2022
[
slides |
picture
]
Keynote
Incremental Solvers for Formal Reasoning
25th Forum on Specification & Design Languages (FDL'22)
Linz, Austria, September 14, 2022
[ slides
]
SAT'22 Test of Time Award for MiniSAT Paper at SAT'03
25th Intl. Conf. on Theory and Applications on Satisfiability Testing (SAT'22)
Haifa, Israel, August 5, 2022
[ slides
]
Invited talk
Trusting SAT Solvers
Session on 25 years of SAT
25th Intl. Conf. on Theory and Applications on Satisfiability Testing (SAT'22)
Haifa, Israel, August 4, 2022
[ slides
]
Scalable Proof Producing Multi-Threaded SAT Solving with
Gimsatul through Sharing instead of Copying Clauses
12th Workshop on Pragmatics of SAT (POS'22)
Haifa, Israel, August 1, 2022
[ slides
| arxiv
| code
| experiments
]
Talks 2021
Mining Definitions in Kissat with Kittens
11th Workshop on Pragmatics of SAT (POS'21)
Cyberspace, July 5, 2021
[ slides
]
Fueling the SAT Revolution
Workshop Verified Software: Tools and Experiments (VSOW04)
Isaac Newton Institute for Mathematical Sciences
Cyberspace, June 8, 2021
[ slides | demo ]
A Personal History of Practical SAT Solving
Workshop 50 Years of Satisfiability: The Centrality of SAT in the Theory of Computing
Program
Satisfiability: Theory, Practice, and Beyond
Simons Institute for the Theory of Computing
Cyberspace, May 13, 2021
[ video ]
Tutorial
SAT-Solving
Satisfiability: Theory, Practice, and Beyond Boot Camp
Program Satisfiability: Theory, Practice, and Beyond
Simons Institute for the Theory of Computing
Cyberspace, February 2, 2021
[
pre-recorded intro on YouTube (4h22) |
local copy of pre-recorded video (4h22) |
live recording on YouTube (2h02) |
code
]
Talks 2020
Tutorial
SAT
5th Indian SAT + SMT Winter School
Cyberspace, December 11, 2020
[ slides
| video 1
| video 2
| video 3
]
Tutorial
Word-Level Model Checking
19th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'20)
Cyberspace, September 21, 2020
[ slides
| video
]
Tutorial
SAT in Master Class
Recent Advances in Optimisation Paradigms and Solving Technology
17th Intl. Conf. on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR'20)
Cyberspace, September 21, 2020
[ slides
| video
]
Armin Biere and Mathias Fleury
Chasing Target Phases
11th Workshop on Pragmatics of SAT (POS'20)
Cyberspace, July 3, 2020
[ slides
| video
| experiments
]
Talks 2019
Invited Talk
Truth Assignments as Conditional Autarkies
Intl. Symp. on Automated Technology for
Verification and Analysis (ATVA'19)
Taipei, Taiwan, Oct. 30, 2019
Tutorial
Conflict-Driven Clause Learning
Intl. Symp. on Automated Technology for
Verification and Analysis (ATVA'19)
Taipei, Taiwan, Oct. 28, 2019
Invited talk
SAT, Computer Algebra, Multipliers
6th Vampire Workshop
Lisbon, Portugal, July 7, 2019
Conflict-Driven Clause Learning
SAT/SMT/AR Summer School 2019
Lisbon, Portugal, July 4, 2019
Invited talk
Algebra, Proofs and Multipliers
28th International Workshop on Logic and Synthesis (IWLS'19)
EPFL Lausanne, Switzerland, June 22, 2019
Tutorial on Modern SAT Solving
Logic Synthesis Software School
EPFL Lausanne, Switzerland, June 20, 2019
Talks 2018
CAV Award talk
Bounded Model Checking and CBMC
30th International Conference on Computer Aided Verification (CAV'18)
Oxford, UK, July 2018
BTOR2, BtorMC and Boolector 3.0
30th International Conference on Computer Aided Verification (CAV'18)
Oxford, UK, July 2018
The Effect on Scrambling CNFs
9th Workshop on Pragmatics of SAT (POS'18)
Oxford, UK, July 2018
Encoding into SAT
SAT/SMT/AR Summer School 2018
International Summer School on Satisfiability, Satisfiability Modulo Theories, and Automated Reasoning
Manchester, UK, July 2018
[
satsmtar18satexercises.tar.gz
|
satsmtar18satsolutions.tar.gz
]
[
satsmtar18satexercises.zip
|
satsmtar18satsolutions.zip
]
Searching, Simplifying, Proving A Tutorial on Modern SAT Solving
European Joint Conferences on Theory and Practice of Software (ETAPS'18)
Thesaloniki, Greece, April 2018
What a Difference a Variable Makes
24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18)
Thesasaloniki, Greece, April 2018
Talks 2017
Learning to Instantiate Quantifiers
Verification Seminars,
Dept. Computer Science,
University of Oxford, December 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
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 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