Resolution-Based Certificate Extraction for QBF - (Tool Presentation). - Aina Niemetz; Mathias Preiner; Florian Lonsing; Martina Seidl; Armin Biere (SAT, 2012)

Lemmas on Demand for Lambdas. - Mathias Preiner; Aina Niemetz; Armin Biere (DIFTS@FMCAD, 2013)

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

Turbo-charging Lemmas on demand with don't care reasoning. - Aina Niemetz; Mathias Preiner; Armin Biere (FMCAD, 2014)

Boolector 2.0. - Aina Niemetz; Mathias Preiner; Armin Biere (J. Satisf. Boolean Model. Comput., 2014)

Better Lemmas with Lambda Extraction. - Mathias Preiner; Aina Niemetz; Armin Biere (FMCAD, 2015)

Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories. - Aina Niemetz; Mathias Preiner; Armin Biere (CAV (1), 2016)

Model-Based API Testing for SMT Solvers. - Aina Niemetz; Mathias Preiner; Armin Biere (SMT, 2017)

Counterexample-Guided Model Synthesis. - Mathias Preiner; Aina Niemetz; Armin Biere (TACAS (1), 2017)

Propagation based local search for bit-precise reasoning. - Aina Niemetz; Mathias Preiner; Armin Biere (Formal Methods Syst. Des., 2017)

Solving Quantified Bit-Vectors Using Invertibility Conditions. - Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (CAV (2), 2018)

Btor2 , BtorMC and Boolector 3.0. - Aina Niemetz; Mathias Preiner; Clifford Wolf; Armin Biere (CAV (1), 2018)

CVC4 at the SMT Competition 2018. - Clark W. Barrett; Haniel Barbosa; Martin Brain; Duligur Ibeling; Tim King 001; Paul Meng; Aina Niemetz; Andres Nötzli; Mathias Preiner; Andrew Reynolds 001; Cesare Tinelli (CoRR, 2018)

Towards Bit-Width-Independent Proofs in SMT Solvers. - Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Yoni Zohar; Clark W. Barrett; Cesare Tinelli (CADE, 2019)

Invertibility Conditions for Floating-Point Formulas. - Martin Brain; Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (CAV (2), 2019)

Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. - Andres Nötzli; Andrew Reynolds 001; Haniel Barbosa; Aina Niemetz; Mathias Preiner; Clark W. Barrett; Cesare Tinelli (SAT, 2019)

DRAT-based Bit-Vector Proofs in CVC4. - Alex Ozdemir; Aina Niemetz; Mathias Preiner; Yoni Zohar; Clark W. Barrett (SAT, 2019)

Ternary Propagation-Based Local Search for more Bit-Precise Reasoning. - Aina Niemetz; Mathias Preiner (FMCAD, 2020)

Abstract: MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers. - Joseph Scott; Aina Niemetz; Mathias Preiner; Vijay Ganesh 001 (SMT, 2020)

Bitwuzla at the SMT-COMP 2020. - Aina Niemetz; Mathias Preiner (CoRR, 2020)

ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends. - Gereon Kremer; Aina Niemetz; Mathias Preiner (CAV (2), 2021)

Syntax-Guided Quantifier Instantiation. - Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (TACAS (2), 2021)

MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers. - Joseph Scott; Aina Niemetz; Mathias Preiner; Saeed Nejati; Vijay Ganesh 001 (TACAS (2), 2021)

On solving quantified bit-vector constraints using invertibility conditions. - Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (Formal Methods Syst. Des., 2021)

Towards Satisfiability Modulo Parametric Bit-vectors. - Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Yoni Zohar; Clark W. Barrett; Cesare Tinelli (J. Autom. Reason., 2021)

Syntax-Guided Quantifier Instantiation (TACAS 2021 Artifact). - Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (Zenodo, 2021)

Flexible Proof Production in an Industrial-Strength SMT Solver. - Haniel Barbosa; Andrew Reynolds 001; Gereon Kremer; Hanna Lachnitt; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; Arjun Viswanathan 001; Scott Viteri; Yoni Zohar; Cesare Tinelli; et al. (IJCAR, 2022)

Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. - Aina Niemetz; Mathias Preiner; Clark W. Barrett (CAV (2), 2022)

Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. - Andres Nötzli; Haniel Barbosa; Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (FMCAD, 2022)

The FMCAD 2022 Student Forum. - Mathias Preiner (FMCAD, 2022)

cvc5: A Versatile and Industrial-Strength SMT Solver. - Haniel Barbosa; Clark W. Barrett; Martin Brain; Gereon Kremer; Hanna Lachnitt; Makai Mann; Abdalrhman Mohamed; Mudathir Mohamed; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; et al. (TACAS (1), 2022)

Bit-Precise Reasoning via Int-Blasting. - Yoni Zohar; Ahmed Irfan; Makai Mann; Aina Niemetz; Andres Nötzli; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (VMCAI, 2022)

Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. - Aina Niemetz; Mathias Preiner; Clark W. Barrett (Zenodo, 2022)

MachSMT: Machine Learning Driven Algorithm Selection for SMT Solvers. - Joseph Scott; Aina Niemetz; Mathias Preiner; Saeed Nejati; Vijay Ganesh 001 (Zenodo, 2022)

Bitwuzla. - Aina Niemetz; Mathias Preiner (CAV (2), 2023)

IPASIR-UP: User Propagators for CDCL. - Katalin Fazekas; Aina Niemetz; Mathias Preiner; Markus Kirchweger; Stefan Szeider; Armin Biere (SAT, 2023)

Algorithm selection for SMT. - Joseph Scott; Aina Niemetz; Mathias Preiner; Saeed Nejati; Vijay Ganesh 001 (Int. J. Softw. Tools Technol. Transf., 2023)

Supplementary material of submission "IPASIR-UP: User Propagators for CDCL". - Katalin Fazekas; Aina Niemetz; Mathias Preiner; Markus Kirchweger; Stefan Szeider; Armin Biere (Zenodo, 2023)

Generating and Exploiting Automated Reasoning Proof Certificates. - Haniel Barbosa; Clark W. Barrett; Byron Cook; Bruno Dutertre; Gereon Kremer; Hanna Lachnitt; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; Andrew Reynolds 001; Cesare Tinelli; et al. (Commun. ACM, 2023)

Publisher Correction: Algorithm selection for SMT. - Joseph Scott; Aina Niemetz; Mathias Preiner; Saeed Nejati; Vijay Ganesh 001 (Int. J. Softw. Tools Technol. Transf., 2023)

Scalable Bit-Blasting with Abstractions. - Aina Niemetz; Mathias Preiner; Yoni Zohar (CAV (1), 2024)

Satisfiability Modulo Theories: A Beginner's Tutorial. - Clark W. Barrett; Cesare Tinelli; Haniel Barbosa; Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Yoni Zohar (FM (2), 2024)

Hardware Model Checking Competition 2024. - Armin Biere; Nils Froleyks; Mathias Preiner (FMCAD, 2024)

Challenges in Bit-Vector Reasoning. - Mathias Preiner (SMT@CAV, 2024)

Using Normalization to Improve SMT Solver Stability. - Daneshvar Amrollahi; Mathias Preiner; Aina Niemetz; Andrew Reynolds 001; Moses Charikar; Cesare Tinelli; Clark W. Barrett (CoRR, 2024)

Satisfiability Modulo User Propagators. - Katalin Fazekas; Aina Niemetz; Mathias Preiner; Markus Kirchweger; Stefan Szeider; Armin Biere (J. Artif. Intell. Res., 2024)

SMT-LIB release 2023 (incremental benchmarks). - Mathias Preiner; Hans-Jörg Schurr; Clark W. Barrett; Pascal Fontaine; Aina Niemetz; Cesare Tinelli (Zenodo, 2024)

SMT-LIB release 2023 (non-incremental benchmarks). - Mathias Preiner; Hans-Jörg Schurr; Clark W. Barrett; Pascal Fontaine; Aina Niemetz; Cesare Tinelli (Zenodo, 2024)

SMT-LIB release 2024 (non-incremental benchmarks). - Mathias Preiner; Hans-Jörg Schurr; Clark W. Barrett; Pascal Fontaine; Aina Niemetz; Cesare Tinelli (Zenodo, 2024)

SMT-LIB release 2024 (incremental benchmarks). - Mathias Preiner; Hans-Jörg Schurr; Clark W. Barrett; Pascal Fontaine; Aina Niemetz; Cesare Tinelli (Zenodo, 2024)

SMT-LIB release 2024 (incremental benchmarks). - Mathias Preiner; Hans-Jörg Schurr; Clark W. Barrett; Pascal Fontaine; Aina Niemetz; Cesare Tinelli (Zenodo, 2024)

cvc5 for SMT-COMP 2024. - Leni Aniva; Haniel Barbosa; Clark W. Barrett; Hanna Lachnitt; Daniel Larraz; Abdalrhman Mohamed; Mudathir Mohamed; Aina Niemetz; Alex Ozdemir; Mathias Preiner; Andrew Reynolds 001; Hans-Jörg Schurr; et al. (Zenodo, 2024)

Supplementary material of "Satisfiability modulo User Propagators". - Katalin Fazekas; Aina Niemetz; Mathias Preiner; Markus Kirchweger; Stefan Szeider; Armin Biere (Zenodo, 2024)

HWMCC'24 Benchmarks and Results. - Mathias Preiner; Nils Froleyks; Armin Biere (Zenodo, 2024)

HWMCC'24 Benchmarks and Results. - Mathias Preiner; Nils Froleyks; Armin Biere (Zenodo, 2024)

HWMCC'24 Benchmarks and Results. - Mathias Preiner; Nils Froleyks; Armin Biere (Zenodo, 2024)

Introducing Certificates to the Hardware Model Checking Competition. - Nils Froleyks; Emily Yu; Mathias Preiner; Armin Biere; Keijo Heljanko (CAV (1), 2025)

Bit-Precise Reasoning with Parametric Bit-Vectors. - Zvika Berger; Yoni Zohar; Aina Niemetz; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (SAT, 2025)

HWMCC'24 Benchmarks and Results. - Mathias Preiner; Nils Froleyks; Armin Biere (Zenodo, 2025)