Mathias Preiner

Publication Activity (10 Years)

Years Active: 2012-2024
Publications (10 Years): 35

Top Topics

Modulo Theories

Top Venues

Publications

Mathias Preiner
Challenges in Bit-Vector Reasoning. SMT@CAV (2024)
Aina Niemetz, Mathias Preiner, Yoni Zohar
Scalable Bit-Blasting with Abstractions. CAV (1) (2024)
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
Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM 66 (10) (2023)
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh
Algorithm selection for SMT. Int. J. Softw. Tools Technol. Transf. 25 (2) (2023)
Aina Niemetz, Mathias Preiner
Bitwuzla. CAV (2) (2023)
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh
Publisher Correction: Algorithm selection for SMT. Int. J. Softw. Tools Technol. Transf. 25 (5) (2023)
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere
IPASIR-UP: User Propagators for CDCL. SAT (2023)
Mathias Preiner
The FMCAD 2022 Student Forum. FMCAD (2022)
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Bit-Precise Reasoning via Int-Blasting. VMCAI (2022)
Aina Niemetz, Mathias Preiner, Clark W. Barrett
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. CAV (2) (2022)
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
cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS (1) (2022)
Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. FMCAD (2022)
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
Flexible Proof Production in an Industrial-Strength SMT Solver. IJCAR (2022)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
Towards Satisfiability Modulo Parametric Bit-vectors. J. Autom. Reason. 65 (7) (2021)
Gereon Kremer, Aina Niemetz, Mathias Preiner
ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends. CAV (2) (2021)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Syntax-Guided Quantifier Instantiation. TACAS (2) (2021)
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh
MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers. TACAS (2) (2021)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
On solving quantified bit-vector constraints using invertibility conditions. Formal Methods Syst. Des. 57 (1) (2021)
Joseph Scott, Aina Niemetz, Mathias Preiner, Vijay Ganesh
Abstract: MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers. SMT (2020)
Aina Niemetz, Mathias Preiner
Ternary Propagation-Based Local Search for more Bit-Precise Reasoning. FMCAD (2020)
Aina Niemetz, Mathias Preiner
Bitwuzla at the SMT-COMP 2020. CoRR (2020)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
Towards Bit-Width-Independent Proofs in SMT Solvers. CADE (2019)
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett
DRAT-based Bit-Vector Proofs in CVC4. CoRR (2019)
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. SAT (2019)
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett
DRAT-based Bit-Vector Proofs in CVC4. SAT (2019)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
Towards Bit-Width-Independent Proofs in SMT Solvers. CoRR (2019)
Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Invertibility Conditions for Floating-Point Formulas. CAV (2) (2019)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
On Solving Quantified Bit-Vectors using Invertibility Conditions. CoRR (2018)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Solving Quantified Bit-Vectors Using Invertibility Conditions. CAV (2) (2018)
Clark W. Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli
CVC4 at the SMT Competition 2018. CoRR (2018)
Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere
Btor2 , BtorMC and Boolector 3.0. CAV (1) (2018)
Mathias Preiner, Aina Niemetz, Armin Biere
Counterexample-Guided Model Synthesis. TACAS (1) (2017)
Aina Niemetz, Mathias Preiner, Armin Biere
Propagation based local search for bit-precise reasoning. Formal Methods Syst. Des. 51 (3) (2017)
Aina Niemetz, Mathias Preiner, Armin Biere
Model-Based API Testing for SMT Solvers. SMT (2017)
Aina Niemetz, Mathias Preiner, Armin Biere
Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories. CAV (1) (2016)
Mathias Preiner, Aina Niemetz, Armin Biere
Better Lemmas with Lambda Extraction. FMCAD (2015)
Aina Niemetz, Mathias Preiner, Armin Biere
Turbo-charging Lemmas on demand with don't care reasoning. FMCAD (2014)
Aina Niemetz, Mathias Preiner, Armin Biere
Boolector 2.0. J. Satisf. Boolean Model. Comput. 9 (1) (2014)
Mathias Preiner, Aina Niemetz, Armin Biere
Lemmas on Demand for Lambdas. DIFTS@FMCAD (2013)
Martin Aigner, Armin Biere, Christoph M. Kirsch, Aina Niemetz, Mathias Preiner
Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures. POS@SAT (2013)
Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere
Resolution-Based Certificate Extraction for QBF - (Tool Presentation). SAT (2012)