default search action

combined dblp search
author search
venue search
publication search

ask others

Mathias Preiner

> Home > Persons

Person information

affiliation: Stanford University, CA, USA
affiliation (former): Johannes Kepler University, Linz, Austria

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

Journal Articles

see FAQ

What is the meaning of the colors in the publication lists?

2024
[j8]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jair/FazekasNPKSB24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jair/FazekasNPKSB24
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere:
Satisfiability Modulo User Propagators. J. Artif. Intell. Res. 81: 989-1017 (2024)
2023
[j7]
- view
  authority control:
- export record
  dblp key:
  - journals/cacm/BarbosaBCDKLNNOPRTZ23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/cacm/BarbosaBCDKLNNOPRTZ23
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): 86-95 (2023)
[j6]
- view
  authority control:
- export record
  dblp key:
  - journals/sttt/ScottNPNG23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/sttt/ScottNPNG23
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh:
Algorithm selection for SMT. Int. J. Softw. Tools Technol. Transf. 25(2): 219-239 (2023)
[j5]
- view
  authority control:
- export record
  dblp key:
  - journals/sttt/ScottNPNG23a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/sttt/ScottNPNG23a
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh:
Publisher Correction: Algorithm selection for SMT. Int. J. Softw. Tools Technol. Transf. 25(5): 799-800 (2023)
2021
[j4]
- view
  authority control:
- export record
  dblp key:
  - journals/fmsd/NiemetzPRBT21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/NiemetzPRBT21
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): 87-115 (2021)
[j3]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/NiemetzP0ZBT21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/NiemetzP0ZBT21
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Towards Satisfiability Modulo Parametric Bit-vectors. J. Autom. Reason. 65(7): 1001-1025 (2021)
2017
[j2]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/fmsd/NiemetzPB17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fmsd/NiemetzPB17
Aina Niemetz, Mathias Preiner, Armin Biere:
Propagation based local search for bit-precise reasoning. Formal Methods Syst. Des. 51(3): 608-636 (2017)
2014
[j1]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jsat/NiemetzPB14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jsat/NiemetzPB14
Aina Niemetz, Mathias Preiner, Armin Biere:
Boolector 2.0. J. Satisf. Boolean Model. Comput. 9(1): 53-58 (2014)

Conference and Workshop Papers

see FAQ

What is the meaning of the colors in the publication lists?

2025
[c33]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/FroleyksYPBH25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/FroleyksYPBH25
Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko:
Introducing Certificates to the Hardware Model Checking Competition. CAV (1) 2025: 281-295
[c32]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/sat/BergerZNP0BT25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/BergerZNP0BT25
Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Bit-Precise Reasoning with Parametric Bit-Vectors. SAT 2025: 4:1-4:24
2024
[c31]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/NiemetzPZ24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/NiemetzPZ24
Aina Niemetz, Mathias Preiner, Yoni Zohar:
Scalable Bit-Blasting with Abstractions. CAV (1) 2024: 178-200
[c30]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fm/BarrettTBNPRZ24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fm/BarrettTBNPRZ24
Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar:
Satisfiability Modulo Theories: A Beginner's Tutorial. FM (2) 2024: 571-596
[c29]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/BiereFP24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/BiereFP24
Armin Biere, Nils Froleyks, Mathias Preiner:
Hardware Model Checking Competition 2024. FMCAD 2024: 1
[c28]
- view
  - electronic edition @ ceur-ws.org (open access)
  - details & citations
- export record
  dblp key:
  - conf/smt/Preiner24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/smt/Preiner24
Mathias Preiner:
Challenges in Bit-Vector Reasoning. SMT@CAV 2024: 2
2023
[c27]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/NiemetzP23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/NiemetzP23
Aina Niemetz, Mathias Preiner:
Bitwuzla. CAV (2) 2023: 3-17
[c26]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/sat/FazekasNPKSB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/FazekasNPKSB23
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere:
IPASIR-UP: User Propagators for CDCL. SAT 2023: 8:1-8:13
2022
[c25]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cade/BarbosaRKLNNOPV22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BarbosaRKLNNOPV22
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: 15-35
[c24]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/NiemetzPB22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/NiemetzPB22
Aina Niemetz, Mathias Preiner, Clark W. Barrett:
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. CAV (2) 2022: 92-106
[c23]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/Preiner22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/Preiner22
Mathias Preiner:
The FMCAD 2022 Student Forum. FMCAD 2022: 5-6
[c22]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/NotzliBNPRBT22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/NotzliBNPRBT22
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: 65-74
[c21]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/BarbosaBBKLMMMN22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/BarbosaBBKLMMMN22
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: 415-442
[c20]
- view
  authority control:
- export record
  dblp key:
  - conf/vmcai/ZoharIMNNPRBT22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vmcai/ZoharIMNNPRBT22
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: 496-518
2021
[c19]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/KremerNP20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/KremerNP20
Gereon Kremer, Aina Niemetz, Mathias Preiner:
ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends. CAV (2) 2021: 231-242
[c18]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/NiemetzPRBT21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/NiemetzPRBT21
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Syntax-Guided Quantifier Instantiation. TACAS (2) 2021: 145-163
[c17]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/ScottNPNG21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/ScottNPNG21
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh:
MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers. TACAS (2) 2021: 303-325
2020
[c16]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/NiemetzP20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/NiemetzP20
Aina Niemetz, Mathias Preiner:
Ternary Propagation-Based Local Search for more Bit-Precise Reasoning. FMCAD 2020: 214-224
[c15]
- view
  - electronic edition @ ceur-ws.org (open access)
  - details & citations
- export record
  dblp key:
  - conf/smt/ScottNPG20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/smt/ScottNPG20
Joseph Scott, Aina Niemetz, Mathias Preiner, Vijay Ganesh:
Abstract: MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers. SMT 2020: 62
2019
[c14]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/NiemetzPRZBT19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/NiemetzPRZBT19
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Towards Bit-Width-Independent Proofs in SMT Solvers. CADE 2019: 366-384
[c13]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/BrainNPRBT19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/BrainNPRBT19
Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Invertibility Conditions for Floating-Point Formulas. CAV (2) 2019: 116-136
[c12]
- view
  authority control:
- export record
  dblp key:
  - conf/sat/NotzliRBNPBT19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/NotzliRBNPBT19
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: 279-297
[c11]
- view
  authority control:
- export record
  dblp key:
  - conf/sat/OzdemirNPZB19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/OzdemirNPZB19
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett:
DRAT-based Bit-Vector Proofs in CVC4. SAT 2019: 298-305
2018
[c10]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/NiemetzPRBT18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/NiemetzPRBT18
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Solving Quantified Bit-Vectors Using Invertibility Conditions. CAV (2) 2018: 236-255
[c9]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/NiemetzPWB18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/NiemetzPWB18
Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere:
Btor2 , BtorMC and Boolector 3.0. CAV (1) 2018: 587-595
2017
[c8]
- view
  - electronic edition @ ceur-ws.org (open access)
  - details & citations
- export record
  dblp key:
  - conf/smt/NiemetzPB17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/smt/NiemetzPB17
Aina Niemetz, Mathias Preiner, Armin Biere:
Model-Based API Testing for SMT Solvers. SMT 2017: 3-14
[c7]
- view
  authority control:
- export record
  dblp key:
  - conf/tacas/PreinerNB17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/PreinerNB17
Mathias Preiner, Aina Niemetz, Armin Biere:
Counterexample-Guided Model Synthesis. TACAS (1) 2017: 264-280
2016
[c6]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/NiemetzPB16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/NiemetzPB16
Aina Niemetz, Mathias Preiner, Armin Biere:
Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories. CAV (1) 2016: 199-217
2015
[c5]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/PreinerNB15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/PreinerNB15
Mathias Preiner, Aina Niemetz, Armin Biere:
Better Lemmas with Lambda Extraction. FMCAD 2015: 128-135
2014
[c4]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/NiemetzPB14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/NiemetzPB14
Aina Niemetz, Mathias Preiner, Armin Biere:
Turbo-charging Lemmas on demand with don't care reasoning. FMCAD 2014: 179-186
2013
[c3]
- view
  - electronic edition @ ceur-ws.org (open access)
  - details & citations
- export record
  dblp key:
  - conf/fmcad/PreinerNB13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/PreinerNB13
Mathias Preiner, Aina Niemetz, Armin Biere:
Lemmas on Demand for Lambdas. DIFTS@FMCAD 2013
[c2]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/sat/AignerBKNP13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/AignerBKNP13
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: 28-40
2012
[c1]
- view
  authority control:
- export record
  dblp key:
  - conf/sat/NiemetzPLSB12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/NiemetzPLSB12
Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere:
Resolution-Based Certificate Extraction for QBF - (Tool Presentation). SAT 2012: 430-435

Editorship

see FAQ

What is the meaning of the colors in the publication lists?

2023
[e1]
- view
- export record
  dblp key:
  - conf/smt/2023
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/smt/2023
Stéphane Graham-Lengrand, Mathias Preiner:
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. CEUR Workshop Proceedings 3429, CEUR-WS.org 2023 [contents]

Data and Artifacts

see FAQ

What is the meaning of the colors in the publication lists?

2025
[d27]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/BarbosaBLMMNNOPRSTWZ25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/BarbosaBLMMNNOPRSTWZ25
Haniel Barbosa, Clark W. Barrett, Hanna Lachnitt, Abdalrhman Mohamed, Mudathir Mohamed, José Neto, Aina Niemetz, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Hans-Jörg Schurr, Cesare Tinelli, Amalee Wilson, Yoni Zohar:
cvc5 for SMT-COMP 2025. Zenodo, 2025
[d26]
- view
  authority control:
- export record
  dblp key:
  - data/11/FroleyksYPBH25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/FroleyksYPBH25
Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko:
Introducing Certificates to the Hardware Model Checking Competition. Version 1. Zenodo, 2025 [all versions]
[d25]
- view
  authority control:
- export record
  dblp key:
  - data/11/FroleyksYPBH25a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/FroleyksYPBH25a
Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko:
Introducing Certificates to the Hardware Model Checking Competition. Version 2. Zenodo, 2025 [all versions]
[d24]
- view
  authority control:
- export record
  dblp key:
  - data/11/FroleyksYPBH25b
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/FroleyksYPBH25b
Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko:
Introducing Certificates to the Hardware Model Checking Competition. Version 3. Zenodo, 2025 [all versions]
[d23]
- view
  authority control:
- export record
  dblp key:
  - data/11/FroleyksYPBH25c
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/FroleyksYPBH25c
Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko:
Introducing Certificates to the Hardware Model Checking Competition. Version 4. Zenodo, 2025 [all versions]
[d22]
- view
  authority control:
- export record
  dblp key:
  - data/11/FroleyksYPBH25d
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/FroleyksYPBH25d
Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko:
Introducing Certificates to the Hardware Model Checking Competition. Version 5. Zenodo, 2025 [all versions]
[d21]
- view
  authority control:
- export record
  dblp key:
  - data/11/FroleyksYPBH25e
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/FroleyksYPBH25e
Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko:
Introducing Certificates to the Hardware Model Checking Competition. Version 6. Zenodo, 2025 [all versions]
[d20]
- view
  authority control:
- export record
  dblp key:
  - data/11/FroleyksYPBH25g
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/FroleyksYPBH25g
Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko:
Introducing Certificates to the Hardware Model Checking Competition. Version 7. Zenodo, 2025 [all versions]
[d19]
- view
  authority control:
- export record
  dblp key:
  - data/11/PreinerFB25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerFB25
Mathias Preiner, Nils Froleyks, Armin Biere:
HWMCC'24 Benchmarks and Results. Version 4. Zenodo, 2025 [all versions]
[d18]
- view
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT25
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2025 (non-incremental benchmarks). Version 2025.05.22. Zenodo, 2025 [all versions]
[d17]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT25a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT25a
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2025 (incremental benchmarks). Zenodo, 2025
[d16]
- view
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT25b
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT25b
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2025 (non-incremental benchmarks). Version 2025.08.04. Zenodo, 2025 [all versions]
[d15]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/SchurrPNBFT25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/SchurrPNBFT25
Hans-Jörg Schurr, Mathias Preiner, Aina Niemetz, Clark W. Barrett, Pascal Fontaine, Cesare Tinelli:
SMT-LIB Catalog 2025. Zenodo, 2025
2024
[d14]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/AnivaBBLLMMNOPRSTWZ24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/AnivaBBLLMMNOPRSTWZ24
Leni Aniva, Haniel Barbosa, Clark W. Barrett, Hanna Lachnitt, Daniel Larraz, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Hans-Jörg Schurr, Cesare Tinelli, Amalee Wilson, Yoni Zohar:
cvc5 for SMT-COMP 2024. Zenodo, 2024
[d13]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/FazekasNPKSB24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/FazekasNPKSB24
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere:
Supplementary material of "Satisfiability modulo User Propagators". Zenodo, 2024
[d12]
- view
  authority control:
- export record
  dblp key:
  - data/11/PreinerFB24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerFB24
Mathias Preiner, Nils Froleyks, Armin Biere:
HWMCC'24 Benchmarks and Results. Version 1. Zenodo, 2024 [all versions]
[d11]
- view
  authority control:
- export record
  dblp key:
  - data/11/PreinerFB24a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerFB24a
Mathias Preiner, Nils Froleyks, Armin Biere:
HWMCC'24 Benchmarks and Results. Version 2. Zenodo, 2024 [all versions]
[d10]
- view
  authority control:
- export record
  dblp key:
  - data/11/PreinerFB24b
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerFB24b
Mathias Preiner, Nils Froleyks, Armin Biere:
HWMCC'24 Benchmarks and Results. Version 3. Zenodo, 2024 [all versions]
[d9]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT24
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2023 (incremental benchmarks). Zenodo, 2024
[d8]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT24a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT24a
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2023 (non-incremental benchmarks). Zenodo, 2024
[d7]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT24b
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT24b
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2024 (non-incremental benchmarks). Zenodo, 2024
[d6]
- view
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT24c
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT24c
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2024 (incremental benchmarks). Version 2024.04.23. Zenodo, 2024 [all versions]
[d5]
- view
  authority control:
- export record
  dblp key:
  - data/11/PreinerSBFNT24d
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/PreinerSBFNT24d
Mathias Preiner, Hans-Jörg Schurr, Clark W. Barrett, Pascal Fontaine, Aina Niemetz, Cesare Tinelli:
SMT-LIB release 2024 (incremental benchmarks). Version 2024.05.13. Zenodo, 2024 [all versions]
2023
[d4]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/10/FazekasNPKSB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/10/FazekasNPKSB23
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere:
Supplementary material of submission "IPASIR-UP: User Propagators for CDCL". Zenodo, 2023
2022
[d3]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/10/NiemetzPB22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/10/NiemetzPB22
Aina Niemetz, Mathias Preiner, Clark W. Barrett:
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. Zenodo, 2022
[d2]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/10/ScottNPNG22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/10/ScottNPNG22
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh:
MachSMT: Machine Learning Driven Algorithm Selection for SMT Solvers. Zenodo, 2022
2021
[d1]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/10/NiemetzPRBT21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/10/NiemetzPRBT21
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Syntax-Guided Quantifier Instantiation (TACAS 2021 Artifact). Zenodo, 2021

Informal and Other Publications

see FAQ

What is the meaning of the colors in the publication lists?

2024
[i6]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2410-22419
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2410-22419
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett:
Using Normalization to Improve SMT Solver Stability. CoRR abs/2410.22419 (2024)
2020
[i5]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2006-01621
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2006-01621
Aina Niemetz, Mathias Preiner:
Bitwuzla at the SMT-COMP 2020. CoRR abs/2006.01621 (2020)
2019
[i4]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1905-10434
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1905-10434
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Towards Bit-Width-Independent Proofs in SMT Solvers. CoRR abs/1905.10434 (2019)
[i3]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1907-00087
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1907-00087
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett:
DRAT-based Bit-Vector Proofs in CVC4. CoRR abs/1907.00087 (2019)
2018
[i2]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1804-05025
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1804-05025
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
On Solving Quantified Bit-Vectors using Invertibility Conditions. CoRR abs/1804.05025 (2018)
[i1]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1806-08775
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1806-08775
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 abs/1806.08775 (2018)

Coauthor Index

see FAQ

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.