Mathias Preiner

53 papers A 7B 9Journal 14Unranked 22
YearRankTypeTitle / Venue / Authors
2026 — conf
Bit-Precise Interpolation in Bitwuzla.
TACAS (1)
Aina Niemetz, Mathias Preiner
2026 — conf
Exploring the SMT-LIB Benchmark Library.
TACAS (1)
Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Clark W. Barrett, Pascal Fontaine, Cesare Tinelli
2026 — conf
Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob.
TACAS (1)
Dominik Schreiber, Aina Niemetz, Mathias Preiner
2025 A conf
Bit-Precise Reasoning with Parametric Bit-Vectors.
SAT
Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2025 B conf
Hardware Model Checking Competition 2025.
FMCAD
Armin Biere, Nils Froleyks, Mathias Preiner
2025 — conf
Introducing Certificates to the Hardware Model Checking Competition.
CAV (1)
Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko
2025 B conf
Towards SMT Solver Stability via Input Normalization.
FMCAD
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett
2024 — conf
Challenges in Bit-Vector Reasoning.
SMT@CAV
Mathias Preiner
2024 B conf
Hardware Model Checking Competition 2024.
FMCAD
Armin Biere, Nils Froleyks, Mathias Preiner
2024 — conf
Satisfiability Modulo Theories: A Beginner's Tutorial.
FM (2)
Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar
2024 J jnl
Satisfiability Modulo User Propagators.
J. Artif. Intell. Res.
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere
2024 — conf
Scalable Bit-Blasting with Abstractions.
CAV (1)
Aina Niemetz, Mathias Preiner, Yoni Zohar
2024 J jnl
Using Normalization to Improve SMT Solver Stability.
CoRR
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett
2023 J jnl
Algorithm selection for SMT.
Int. J. Softw. Tools Technol. Transf.
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh
2023 — conf
Bitwuzla.
CAV (2)
Aina Niemetz, Mathias Preiner
2023 J jnl
Generating and Exploiting Automated Reasoning Proof Certificates.
Commun. ACM
Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar
2023 A conf
IPASIR-UP: User Propagators for CDCL.
SAT
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere
2023 — ed.
Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on Automated Deduction (CADE 2023), Rome, Italy, July, 5-6, 2023.
SMT
Stéphane Graham-Lengrand, Mathias Preiner
2023 J jnl
Publisher Correction: Algorithm selection for SMT.
Int. J. Softw. Tools Technol. Transf.
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh
2022 B conf
Bit-Precise Reasoning via Int-Blasting.
VMCAI
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022 A conf
Flexible Proof Production in an Industrial-Strength SMT Solver.
IJCAR
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 W. Barrett
2022 — conf
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers.
CAV (2)
Aina Niemetz, Mathias Preiner, Clark W. Barrett
2022 B conf
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language.
FMCAD
Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022 B conf
The FMCAD 2022 Student Forum.
FMCAD
Mathias Preiner
2022 — conf
cvc5: A Versatile and Industrial-Strength SMT Solver.
TACAS (1)
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, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar
2021 — conf
MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers.
TACAS (2)
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh
2021 J jnl
On solving quantified bit-vector constraints using invertibility conditions.
Formal Methods Syst. Des.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021 — conf
Syntax-Guided Quantifier Instantiation.
TACAS (2)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021 J jnl
Towards Satisfiability Modulo Parametric Bit-vectors.
J. Autom. Reason.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2021 — conf
ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends.
CAV (2)
Gereon Kremer, Aina Niemetz, Mathias Preiner
2020 — conf
Abstract: MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers.
SMT
Joseph Scott, Aina Niemetz, Mathias Preiner, Vijay Ganesh
2020 J jnl
Bitwuzla at the SMT-COMP 2020.
CoRR
Aina Niemetz, Mathias Preiner
2020 B conf
Ternary Propagation-Based Local Search for more Bit-Precise Reasoning.
FMCAD
Aina Niemetz, Mathias Preiner
2019 A conf
DRAT-based Bit-Vector Proofs in CVC4.
SAT
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett
2019 J jnl
DRAT-based Bit-Vector Proofs in CVC4.
CoRR
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett
2019 — conf
Invertibility Conditions for Floating-Point Formulas.
CAV (2)
Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2019 A conf
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers.
SAT
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli
2019 A conf
Towards Bit-Width-Independent Proofs in SMT Solvers.
CADE
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2019 J jnl
Towards Bit-Width-Independent Proofs in SMT Solvers.
CoRR
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2018 — conf
Btor2 , BtorMC and Boolector 3.0.
CAV (1)
Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere
2018 J jnl
CVC4 at the SMT Competition 2018.
CoRR
Clark W. Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli
2018 J jnl
On Solving Quantified Bit-Vectors using Invertibility Conditions.
CoRR
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2018 — conf
Solving Quantified Bit-Vectors Using Invertibility Conditions.
CAV (2)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2017 — conf
Counterexample-Guided Model Synthesis.
TACAS (1)
Mathias Preiner, Aina Niemetz, Armin Biere
2017 — conf
Model-Based API Testing for SMT Solvers.
SMT
Aina Niemetz, Mathias Preiner, Armin Biere
2017 J jnl
Propagation based local search for bit-precise reasoning.
Formal Methods Syst. Des.
Aina Niemetz, Mathias Preiner, Armin Biere
2016 — conf
Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories.
CAV (1)
Aina Niemetz, Mathias Preiner, Armin Biere
2015 B conf
Better Lemmas with Lambda Extraction.
FMCAD
Mathias Preiner, Aina Niemetz, Armin Biere
2014 J jnl
Boolector 2.0.
J. Satisf. Boolean Model. Comput.
Aina Niemetz, Mathias Preiner, Armin Biere
2014 B conf
Turbo-charging Lemmas on demand with don't care reasoning.
FMCAD
Aina Niemetz, Mathias Preiner, Armin Biere
2013 — conf
Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures.
POS@SAT
Martin Aigner, Armin Biere, Christoph M. Kirsch, Aina Niemetz, Mathias Preiner
2013 — conf
Lemmas on Demand for Lambdas.
DIFTS@FMCAD
Mathias Preiner, Aina Niemetz, Armin Biere
2012 A conf
Resolution-Based Certificate Extraction for QBF - (Tool Presentation).
SAT
Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere