Publications
[ Armin Biere | Tobias Faller | Mathias Fleury | Tobias Paxian | Peter Winterer ]
Publication lists of other team members are available from their team home-pages.
2023
Mathias Fleury and
Peter Lammich,
A more Pragmatic CDCL for IsaSAT and targetting LLVM (Short Paper) in
CADE30, 2023,
to appear
[ preprint |
Springer (upcoming)
]
Nils Froleyks,
Emily Yu,
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 |
doi |
kb3 |
benchmarks
]
Emily Yu,
Nils Froleyks,
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 |
doi |
chmc |
certifaiger
]
Armin Biere and
Mathias Fleury and
Nils Froleyks and
Marijn Heule.
The SAT Museum.
In Proceedings of the 14th International 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 Proceedings of the 14th International 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 and
Mathias Fleury and
Florian Pollitt.
CaDiCaL_vivinst, IsaSAT, Gimsatul, Kissat, and TabularaSAT Entering
the SAT Competition 2023.
In Proceedings of 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 and
Mathias Fleury and
Armin Biere.
Verifying Floating-Point Commutativity with GRS.
In Proceedings of 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 53,
University of Helsinki 2023.
[ paper
| bibtex
]
Florian Pollitt and
Mathias Fleury.
Armin Biere.
Faster LRAT Checking Than Solving with CaDiCaL.
To be published in
Proc. 26th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'23),
LIPics 2023.
[ bibtex
| drops
| paper
]
Muhammad Osama, Anton Wijs and Armin Biere.
Certified SAT solving with GPU accelerated Inprocessing.
To be published in
Formal Methods in System Design,
Springer.
[ paper
| bibtex
| parafrost
| doi
]
Highlighted paper
Katalin Fazekas and
Aina Niemetz and
Mathias Preiner and
Markus Kirchweger and
Stefan Szeider and
Armin Biere.
IPASIR-Up: User Propagators for CDCL.
To be pubsliehd in
Proc. 26th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'23),
LIPics 2023.
[ preprint
| bibtex
]
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,
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,
pages 133-144,
Springer 2023.
[ paper
| doi
| bibtex ]
Mathias Fleury, Armin Biere.
Mining Definitions in Kissat with Kittens.
To be published in
Formal Methods in System Design,
Springer.
[ preprint
| paper
| data
| doi
]
Florian Pollitt,
Mathias Fleury, and Armin Biere.
Efficient Proof Checking with LRAT in CaDiCaL (Work in Progress)
presented at
MBMV'23.
[
paper |
bibtex
]
Emily Yu, Nils Froleyks, Armin Biere and Keijo Heljanko.
Stratified Certification for k-Induction (Extended Abstract)
presented at
MBMV'23.
[
paper |
bibtex |
certifaiger
]
2022
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),
LIPics 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,
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,
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.