Publications
[ Armin Biere | Tobias Faller | Mathias Fleury | Tobias Paxian | Peter Winterer ]
Publication lists of other team members are available from their team home-pages.
2024
Katalin Fazekas, Florian Pollitt, Mathias Fleury and Armin Biere.
Incremental Proofs for Bounded Model Checking.
To appear in 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
]
Nils Froleyks, Emily Yu and Armin Biere.
Ternary Simulation as Abstract Interpretation (Work in Progress).
To appear in 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
]
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere.
Disjoint Partial Enumeration without Blocking Clauses.
To appear in Proc. AAAI'24, 10 pages, AAAI Press 2024.
[ preprint
| zenodo
]
2023
Mathias Fleury and
Peter Lammich,
A more Pragmatic CDCL for IsaSAT and targetting LLVM (Short Paper).
In Proc. 29th Intl. Conf. on Automated Deduction (CADE'23),
Lecture Notes in Computer Science (LNCS),
vol. 14132,
pages 207-219,
Springer 2023.
[ preprint
]
Nils Froleyks,
Emily Yu and
Armin Biere.
BIG Backbones.
In Proc. 23rd Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'23),
pages 162-167,
vol. 4,
TU Vienna Academic Press,
2023.
[
paper |
bibtex |
doi |
kb3 |
benchmarks
]
Emily Yu,
Nils Froleyks and
Armin Biere.
Towards Compositional Hardware Model Checking Certification.
In Proc. 23rd Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'23),
pages 44-54,
vol. 4,
TU Vienna Academic Press,
2023.
[
paper |
bibtex |
doi |
chmc |
certifaiger
]
Muhammad Osama, Anton Wijs and Armin Biere.
Certified SAT solving with GPU accelerated Inprocessing.
In
Formal Methods in System Design,
Springer.
[ paper
| bibtex
| parafrost
| doi
]
Armin Biere,
Mathias Fleury,
Nils Froleyks and
Marijn Heule.
The SAT Museum.
In Proc. 14th Intl. Workshop on Pragmatics of SAT (POS'23),
vol. 3545, CEUR Workshop Proceedings,
pages 72-87,
CEUR-WS.org 2023.
[ paper
| bibtex
| data
| zenodo
| ceur
]
Tobias Paxian and
Armin Biere.
Uncovering and Classifying Bugs in MaxSAT Solvers through Fuzzing and Delta Debugging.
In Proc. 14th Intl. Workshop on Pragmatics of SAT (POS'23),
vol. 3545, CEUR Workshop Proceedings,
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.
In Proc. SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions,
Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors),
vol. B-2023-1 of Department of Computer Science Report Series B,
pages 14-15,
University of Helsinki, 2023.
[ paper
| bibtex
]
Robin Trüby,
Mathias Fleury and
Armin Biere.
Verifying Floating-Point Commutativity with GRS.
In Proc. SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions,
Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors),
vol. B-2023-1 of Department of Computer Science Report Series B,
page 53,
University of Helsinki, 2023.
[ paper
| bibtex
]
Florian Pollitt,
Mathias Fleury and
Armin Biere.
Faster LRAT Checking Than Solving with CaDiCaL.
In
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
Katalin Fazekas,
Aina Niemetz,
Mathias Preiner,
Markus Kirchweger,
Stefan Szeider and
Armin Biere.
IPASIR-Up: User Propagators for CDCL.
In
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
]
Armin Biere, Nils Froleyks and Wenxi Wang.
CadiBack: Extracting Backbones with CaDiCaL.
In
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
]
Maximilian Heisinger,
Martina Seidl
and
Armin Biere.
ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving.
In 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
]
Daniela Kaufmann
and
Armin Biere.
Improving Amulet2 for Verifying Multiplier Circuits using SAT Solving and Computer Algebra.
In
International Journal on Software Tools for Technology Transfer
vol. 25(2),
pages 133-144,
Springer 2023.
[ paper
| doi
| bibtex ]
Florian Pollitt,
Mathias Fleury, and Armin Biere.
Efficient Proof Checking with LRAT in CaDiCaL (Work in Progress).
In 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).
In 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
Daniela Kaufmann,
Mathias Fleury,
Armin Biere,
Manuel Kauers.
Practical Algebraic Calculus and Nullstellensatz with the Checkers Pacheck and Pastèque and Nuss-Check.
To be published
in Journal of
Formal Methods in System Design,
Springer 2022.
[ preprint
| bibtex
| doi
]
Mathias Fleury,
Armin Biere.
Mining Definitions in Kissat with Kittens.
In Journal of
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
In Proc. 22nd Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'22),
pages 59-64,
vol. 3,
TU Vienna Academic Press
2022.
[
paper |
bibtex |
certifaiger
]
Shaowei Cai, Xindi Zhang, Mathias Fleury and Armin Biere.
Better Decision Heuristics in CDCL through Local Search and Target Phases.
Journal of Artificial Intelligence Research (JAIR).
vol. 74,
pages 1515-1563,
2022.
[ paper
| doi
| bibtex
| code
| data
]
Maximilian Heisinger and
Martina Seidl and
Armin Biere.
.
In Proceedings of the Workshop on Practical Aspects of Automated Reasoning,
vol. 3201, CEUR Workshop Proceedings,
CEUR-WS.org 2022.
[ paper
| bibtex
| quapi
| ceur
]
Mathias Fleury
and
Armin Biere.
Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses.
CoRR abs/2207.13577 (2022), presented at
12th Workshop on Pragmatics of SAT (POS'22).
[ paper
| arxiv
| bibtex
| gimsatul
| slides
]
Armin Biere and Mathias Fleury.
Gimsatul, IsaSAT and Kissat entering the SAT Competition 2022.
In Proc. of SAT Competition 2022 - Solver and Benchmark Descriptions,
Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors),
vol. B-2022-1 of Department of Computer Science Report Series B,
pages 10-11,
University of Helsinki, 2022.
[ paper
| bibtex
]
Emily Yu,
Nils Froleyks,
Armin Biere and
Mathias Fleury.
Hardware Model Checking Certificates.
In Proc. of SAT Competition 2022 - Solver and Benchmark Descriptions,
Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors),
vol. B-2022-1 of Department of Computer Science Report Series B,
page 46,
University of Helsinki, 2022.
[ paper
| bibtex
]
Armin Biere,
Md Solimul Chowdhury,
Marijn J. H. Heule,
Benjamin Kiesl
and Michael W. Whalen.
Migrating Solver State.
In 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
]
Daniela Kaufmann and Armin Biere.
Fuzzing and Delta Debugging And-Inverter Graph Verification Tools,
In 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
]
Randal E. Bryant and Armin Biere and Marijn J. H. Heule.
Clausal Proofs for Pseudo-Boolean Reasoning.
In Proc. 28th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
vol. 13243,
pages 443-461,
Lecture Notes in Computer Science (LNCS),
Springer 2022.
[ paper
| bibtex
| github
| zenodo
]
Daniela Kaufmann, Paul Beame, Armin Biere, Jakob Nordström.
Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification.
In Proc. Design, Automation and Test in Europe (DATE'22),
IEEE 2022.
[ paper
| bibtex
| experiments
]
2021
Nils Froleyks and Armin Biere.
Single Clause Assumption without Activation Literals to Speed-up IC3.
In Proc. 21st Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'21),
pages 72-76,
vol. 2,
TU Vienna Academic Press
2021.
[
paper |
bibtex |
experiments |
cadical
]
Publications before 2022 are listed on the IRA Publication web-page.