Aina Niemetz

54 papers A* 1A 7B 8Journal 15Unranked 21
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 B ed.
Automated Technology for Verification and Analysis - 22nd International Symposium, ATVA 2024, Kyoto, Japan, October 21-25, 2024, Proceedings, Part I
ATVA
S. Akshay, Aina Niemetz, Sriram Sankaranarayanan
2025 — ed.
Automated Technology for Verification and Analysis - 22nd International Symposium, ATVA 2024, Kyoto, Japan, October 21-25, 2024, Proceedings, Part II
ATVA (2)
S. Akshay, Aina Niemetz, Sriram Sankaranarayanan
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
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
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 B conf
Tackling Scalability Issues in Bit-Vector Reasoning.
FMCAD
Aina Niemetz
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 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
Invited Talk: Local Search for Bit-Precise Reasoning and Beyond.
SMT
Aina Niemetz
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 — 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 — ed.
Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021), Online (initially located in Los Angeles, USA), July 18-19, 2021.
SMT
Alexander Nadel, Aina Niemetz
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 A* conf
Creating an Agile Hardware Design Flow.
DAC
Rick Bahr, Clark W. Barrett, Nikhil Bhagdikar, Alex Carsello, Ross Daly, Caleb Donovick, David Durst, Kayvon Fatahalian, Kathleen Feng, Pat Hanrahan, Teguh Hofstee, Mark Horowitz, Dillon Huff, Fredrik Kjolstad, Taeyoung Kong, Qiaoyi Liu, Makai Mann, Jackson Melchert, Ankita Nayak, Aina Niemetz, Gedeon Nyengele, Priyanka Raina, Stephen Richardson, Rajsekhar Setaluri, Jeff Setter, Kavya Sreedhar, Maxwell Strange, James Thomas, Christopher Torng, Leonard Truong, Nestan Tsiskaridze, Keyi Zhang
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 J jnl
The SMT Competition 2015-2018.
J. Satisf. Boolean Model. Comput.
Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, Giles Reger
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