Publications

Bit-Precise Interpolation in Bitwuzla.
Aina Niemetz, Mathias Preiner. TACAS (I): 66--68. (2026)
PDF DOI Bibtex Artifact Bitwuzla

Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob.
Dominik Schreiber, Aina Niemetz, Mathias Preiner. TACAS (I): 170--191. (2026)
ETAPS Best Tool Paper Award
TACAS Distinguished Paper Award
TACAS Distinguished Artifact Award
PDF DOI Bibtex Artifact Bitwuzla

Exploring the SMT-LIB Benchmark Library.
Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Clark Barrett, Pascal Fontaine, Cesare Tinelli. TACAS (I): 150--169. (2026)
PDF DOI Bibtex Artifact

Towards SMT Solver Stability via Input Normalization.
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark Barrett. FMCAD: 84-93. (2025)
PDF DOI Preprint Bibtex Artifact cvc5

Bit-Precise Reasoning with Parametric Bit-Vectors.
Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli. SAT: 4:1--4:24. (2025)
PDF DOI Bibtex Artifact cvc5

Introducing Certificates to the Hardware Model Checking Competition.
Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko. CAV: 281-295. (2025)
Distinguished Paper Award
PDF DOI Bibtex Artifact

Satisfiability Modulo User Propagators.
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere. JAIR: 989--1017. (2024)
PDF DOI Bibtex Artifact CaDiCaL cvc5

Satisfiability Modulo Theories: A Beginner's Tutorial.
Clark Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar. FM: 571-596. (2024)
Distinguished Tutorial Paper Award
PDF DOI Bibtex Artifact cvc5

Scalable Bit-Blasting with Abstractions.
Aina Niemetz, Mathias Preiner, Yoni Zohar. CAV (1): 178-200. (2024)
PDF DOI Bibtex Artifact Bitwuzla

Generating and Exploiting Automated Reasoning Proof Certificates.
Haniel Barbosa, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar. Commun. ACM: 86-95. (2023)
PDF DOI Bibtex cvc5

Bitwuzla.
Aina Niemetz, Mathias Preiner. CAV (II): 3-17. (2023)
CAV Distinguished Paper Award
PDF DOI Bibtex Artifact Bitwuzla

IPASIR-UP: User Propagators for CDCL.
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere. SAT: 8:1--8:13. (2023)
SAT Highlighted Paper
PDF DOI Bibtex Artifact CaDiCaL cvc5

Algorithm Selection for SMT.
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh. STTT: 219-239. (2023)
PDF DOI Bibtex Artifact MachSMT

Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language.
Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Clark Barrett. FMCAD: 65-74. (2022)
PDF DOI Bibtex cvc5

Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers.
Aina Niemetz, Mathias Preiner, Clark Barrett. CAV: 92-106. (2022)
PDF DOI Bibtex Artifact Talk Murxla

Flexible Proof Production in an Industrial-Strength SMT Solver.
Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark Barrett. IJCAR: 15-35. (2022)
PDF DOI Bibtex cvc5

cvc5: A Versatile and Industrial-Strength SMT Solver.
Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar. TACAS: 415-442. (2022)
SCP Best Tool Paper Award
PDF DOI Bibtex Artifact cvc5

Bit-Precise Reasoning via Int-Blasting.
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli. VMCAI: 496-518. (2022)
PDF DOI Bibtex Artifact cvc5

Towards Satisfiability Modulo Parametric Bit-Vectors.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, Cesare Tinelli. JAR 65 (7): 1001-1035. (2021)
PDF DOI Bibtex Artifact CVC4

ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends.
Gereon Kremer, Aina Niemetz, Mathias Preiner. CAV: 231-242. (2021)
PDF DOI Bibtex Artifact ddSMT

Syntax-Guided Quantifier Instantiation.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli. TACAS: 145--163. (2021)
Nominated for the EATCS Best ETAPS Theory Paper Award
PDF DOI Bibtex Artifact CVC4

MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers.
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh. TACAS: 303--325. (2021)
PDF DOI Bibtex Artifact MachSMT

On Solving Quantified Bit-Vector Constraints using Invertibility Conditions.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli. FMSD 57 (1): 87-115. (2021)
PDF DOI Bibtex Artifact CVC4

Ternary Propagation-Based Local Search for More Bit-Precise Reasoning.
Aina Niemetz, Mathias Preiner. FMCAD 2020: 214-224. (2020)
PDF DOI Bibtex Artifact Talk Bitwuzla

CVC4 at the SMT competition 2020.
Clark Barrett, Haniel Barbosa, Martin Brain, Ahmed Irfan, Makai Mann, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Amalee Wilson, Yoni Zohar. SMT 2020. (2020)
PDF Bibtex CVC4

Bitwuzla at the SMT-COMP 2020.
Aina Niemetz, Mathias Preiner. CoRR abs/2006.01621. (2020)
PDF Arxiv Bibtex Bitwuzla

Towards Bit-Width-Independent Proofs in SMT Solvers.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, Cesare Tinelli. CADE 27. (2019)
PDF DOI Arxiv Bibtex CVC4

Invertibility Conditions for Floating-Point Formulas.
Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli. CAV 2019: 116-136. (2019)
PDF DOI Preprint Extended Version Bibtex Artifact CVC4

Syntax-Guided Rewrite Rule Enumeration for SMT Solvers.
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett, Cesare Tinelli. SAT 2019: 279-297. (2019)
PDF DOI Bibtex CVC4

DRAT-based Bit-Vector Proofs in CVC4.
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark Barrett. SAT 2019: 298-305. (2019)
PDF DOI Arxiv Bibtex CVC4

Boolector at the SMT competition 2019.
Aina Niemetz, Mathias Preiner, Armin Biere. SMT 2019. (2019)
PDF Bibtex Boolector

CVC4 at the SMT competition 2019.
Clark Barrett, Haniel Barbosa, Martin Brain, Tim King, Makai Mann, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar. SMT 2019. (2019)
PDF Bibtex CVC4

Solving Quantified Bit-Vectors Using Invertibility Conditions.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli. CAV 2018: 236-255. (2018)
PDF DOI Preprint Extended Version Bibtex Artifact CVC4

Btor2 , BtorMC and Boolector 3.0.
Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere. CAV 2018: 587-595. (2018)
PDF DOI Preprint Bibtex Artifact Boolector

Rewrites for SMT Solvers using Syntax-Guided Enumeration (Work in Progress).
Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Andres Nötzli, Mathias Preiner, Clark Barrett, Cesare Tinelli. SMT 2018. (2018)
PDF Bibtex CVC4

CVC4 at the SMT Competition 2018.
Clark Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli. CoRR abs/1806.08775. (2018)
PDF Arxiv Bibtex CVC4

Boolector at the SMT competition 2018.
Aina Niemetz, Mathias Preiner, Armina Biere. FMV Reports Series, Technical Report 18/1. (2018)
PDF Bibtex Boolector

Propagation based local search for bit-precise reasoning.
Aina Niemetz, Mathias Preiner, Armin Biere. Formal Methods in System Design (FMSD) 51 (3): 608-636. (2017)
PDF DOI Preprint Bibtex Artifact Boolector

Model-Based API Testing for SMT Solvers.
Aina Niemetz, Mathias Preiner, Armin Biere. SMT 2017. (2017)
PDF Bibtex Talk Boolector

Boolector at the SMT competition 2017.
Aina Niemetz, Mathias Preiner, Armin Biere. FMV Reports Series, Technical Report 17/1. (2017)
PDF Bibtex Boolector

Counterexample-Guided Model Synthesis.
Mathias Preiner, Aina Niemetz, Armin Biere. TACAS 2017: 264-280. (2017)
PDF DOI Bibtex Artifact Boolector

Lambdas, Arrays and Quantifiers.
Mathias Preiner. Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University Linz. (2017)
PDF Bibtex Boolector

Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories.
Aina Niemetz, Mathias Preiner, Armin Biere. CAV 2016: 199-217. (2016)
PDF DOI Bibtex Artifact Talk Boolector

Boolector at the SMT competition 2016.
Aina Niemetz, Mathias Preiner, Armin Biere. FMV Reports Series, Technical Report 16/1. (2016)
PDF Bibtex Boolector

Better Lemmas with Lambda Extraction.
Mathias Preiner, Aina Niemetz, Armin Biere. FMCAD 2015: 128-135. (2015)
PDF Bibtex Boolector

Improving Local Search For Bit-Vector Logics in SMT with Path Propagation.
Aina Niemetz, Mathias Preiner, Andreas Fröhlich, Armin Biere. DIFTS 2015. (2015)
PDF Bibtex Artifact Boolector

Boolector at the SMT competition 2015.
Aina Niemetz, Mathias Preiner, Armin Biere. FMV Reports Series, Technical Report 15/1. (2015)
PDF Bibtex Boolector

Boolector 2.0 system description.
Aina Niemetz, Mathias Preiner, Armin Biere. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 9 (1): 53-58. (2014)
PDF DOI Preprint Bibtex Boolector

Turbo-charging Lemmas on Demand with Don't Care Reasoning.
Aina Niemetz, Mathias Preiner, Armin Biere. FMCAD 2014: 179-186. (2014)
PDF DOI Bibtex Artifact Boolector

Boolector at the SMT competition 2014.
Aina Niemetz, Mathias Preiner, Armin Biere. FMV Report Series, Technical Report 14/1. (2014)
PDF Bibtex Boolector

Lemmas on Demand for Lambdas.
Mathias Preiner, Aina Niemetz, Armin Biere. DIFTS 2013. (2013)
PDF Bibtex Artifact Boolector

Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures.
Martin Aigner, Armin Biere, Christoph M. Kirsch, Aina Niemetz, Mathias Preiner. POS 2013. (2013)
PDF Bibtex

Resolution-Based Certificate Extraction for QBF - (Tool Presentation).
Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere. SAT 2012: 430-435. (2012)
PDF DOI Bibtex QBFcert