Mathias Preiner
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
37
Venues
7
Active years
2012–2026
Best venue rank
A*
Where they publish
Papers
37 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | CAV | Satisfiability Modulo Extensional Constant Arrays. | Mathias Preiner, Aina Niemetz, Clark W. Barrett |
| 2026 | CAV | The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver. | Andrew Reynolds, Hans-Jrg Schurr, Haniel Barbosa, Ofec Israel, Jibiana Jakpor, Hanna Lachnitt, Abdalrhman Mohamed, Aina Niemetz, Mathias Preiner, Yoni Zohar, Robert B. Jones, Clark W. Barrett, Cesare Tinelli |
| 2026 | TACAS | Bit-Precise Interpolation in Bitwuzla. | Aina Niemetz, Mathias Preiner |
| 2026 | TACAS | Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob. | Dominik Schreiber, Aina Niemetz, Mathias Preiner |
| 2026 | TACAS | Exploring the SMT-LIB Benchmark Library. | Hans-Jrg Schurr, Franois Bobot, Mathias Preiner, Aina Niemetz, Clark W. Barrett, Pascal Fontaine, Cesare Tinelli |
| 2025 | CAV | Introducing Certificates to the Hardware Model Checking Competition. | Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko |
| 2025 | FMCAD | Towards SMT Solver Stability via Input Normalization. | Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett |
| 2025 | FMCAD | Hardware Model Checking Competition 2025. | Armin Biere, Nils Froleyks, Mathias Preiner |
| 2025 | SAT | Bit-Precise Reasoning with Parametric Bit-Vectors. | Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2024 | CAV | Scalable Bit-Blasting with Abstractions. | Aina Niemetz, Mathias Preiner, Yoni Zohar |
| 2024 | FM | Satisfiability Modulo Theories: A Beginner's Tutorial. | Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar |
| 2024 | FMCAD | Hardware Model Checking Competition 2024. | Armin Biere, Nils Froleyks, Mathias Preiner |
| 2023 | CAV | Bitwuzla. | Aina Niemetz, Mathias Preiner |
| 2023 | SAT | IPASIR-UP: User Propagators for CDCL. | Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere |
| 2022 | CADE | Flexible Proof Production in an Industrial-Strength SMT Solver. | Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Ntzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett |
| 2022 | CAV | Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. | Aina Niemetz, Mathias Preiner, Clark W. Barrett |
| 2022 | FMCAD | Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. | Andres Ntzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2022 | FMCAD | The FMCAD 2022 Student Forum. | Mathias Preiner |
| 2022 | TACAS | 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 Ntzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar |
| 2022 | VMCAI | Bit-Precise Reasoning via Int-Blasting. | Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Ntzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2021 | CAV | ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends. | Gereon Kremer, Aina Niemetz, Mathias Preiner |
| 2021 | TACAS | Syntax-Guided Quantifier Instantiation. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2021 | TACAS | MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers. | Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh |
| 2020 | FMCAD | Ternary Propagation-Based Local Search for more Bit-Precise Reasoning. | Aina Niemetz, Mathias Preiner |
| 2019 | CADE | Towards Bit-Width-Independent Proofs in SMT Solvers. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli |
| 2019 | CAV | Invertibility Conditions for Floating-Point Formulas. | Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2019 | SAT | Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. | Andres Ntzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli |
| 2019 | SAT | DRAT-based Bit-Vector Proofs in CVC4. | Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett |
| 2018 | CAV | Solving Quantified Bit-Vectors Using Invertibility Conditions. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2018 | CAV | Btor2 , BtorMC and Boolector 3.0. | Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere |
| 2017 | TACAS | Counterexample-Guided Model Synthesis. | Mathias Preiner, Aina Niemetz, Armin Biere |
| 2016 | CAV | Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories. | Aina Niemetz, Mathias Preiner, Armin Biere |
| 2015 | FMCAD | Better Lemmas with Lambda Extraction. | Mathias Preiner, Aina Niemetz, Armin Biere |
| 2014 | FMCAD | Turbo-charging Lemmas on demand with don't care reasoning. | Aina Niemetz, Mathias Preiner, Armin Biere |
| 2013 | FMCAD | Lemmas on Demand for Lambdas. | Mathias Preiner, Aina Niemetz, Armin Biere |
| 2013 | SAT | Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures. | Martin Aigner, Armin Biere, Christoph M. Kirsch, Aina Niemetz, Mathias Preiner |
| 2012 | SAT | Resolution-Based Certificate Extraction for QBF - (Tool Presentation). | Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere |