Aina Niemetz

According to our database, Aina Niemetz authored at least 45 papers between 2012 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2024

Using Normalization to Improve SMT Solver Stability.

Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett

CoRR, 2024

Satisfiability Modulo Theories: A Beginner's Tutorial.

Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar

Proceedings of the Formal Methods - 26th International Symposium, 2024

Scalable Bit-Blasting with Abstractions.

Aina Niemetz, Mathias Preiner, Yoni Zohar

Proceedings of the Computer Aided Verification - 36th International Conference, 2024

2023

Publisher Correction: Algorithm selection for SMT.

Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh

Int. J. Softw. Tools Technol. Transf., December, 2023

Generating and Exploiting Automated Reasoning Proof Certificates.

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

Commun. ACM, October, 2023

Supplementary material of submission "IPASIR-UP: User Propagators for CDCL".

Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere

Dataset, June, 2023

Algorithm selection for SMT.

Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh

Int. J. Softw. Tools Technol. Transf., April, 2023

IPASIR-UP: User Propagators for CDCL.

Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere

Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing, 2023

Bitwuzla.

Aina Niemetz, Mathias Preiner

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022

MachSMT: Machine Learning Driven Algorithm Selection for SMT Solvers.

Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh

Dataset, November, 2022

Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers.

Aina Niemetz, Mathias Preiner, Clark W. Barrett

Dataset, May, 2022

Bit-Precise Reasoning via Int-Blasting.

Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2022

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 Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Invited Talk: Local Search for Bit-Precise Reasoning and Beyond.

Aina Niemetz

Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), 2022

Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language.

Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers.

Aina Niemetz, Mathias Preiner, Clark W. Barrett

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Flexible Proof Production in an Industrial-Strength SMT Solver.

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

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

Syntax-Guided Quantifier Instantiation (TACAS 2021 Artifact).

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Dataset, February, 2021

Towards Satisfiability Modulo Parametric Bit-vectors.

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli

J. Autom. Reason., 2021

On solving quantified bit-vector constraints using invertibility conditions.

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Formal Methods Syst. Des., 2021

MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers.

Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

Syntax-Guided Quantifier Instantiation.

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends.

Gereon Kremer, Aina Niemetz, Mathias Preiner

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

Bitwuzla at the SMT-COMP 2020.

Aina Niemetz, Mathias Preiner

CoRR, 2020

Abstract: MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers.

Joseph Scott, Aina Niemetz, Mathias Preiner, Vijay Ganesh

Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020

Ternary Propagation-Based Local Search for more Bit-Precise Reasoning.

Aina Niemetz, Mathias Preiner

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

Creating an Agile Hardware Design Flow.

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

Proceedings of the 57th ACM/IEEE Design Automation Conference, 2020

2019

The SMT Competition 2015-2018.

Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, Giles Reger

J. Satisf. Boolean Model. Comput., 2019

DRAT-based Bit-Vector Proofs in CVC4.

Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Syntax-Guided Rewrite Rule Enumeration for SMT Solvers.

Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Invertibility Conditions for Floating-Point Formulas.

Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Towards Bit-Width-Independent Proofs in SMT Solvers.

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli

Proceedings of the Automated Deduction - CADE 27, 2019

2018

CVC4 at the SMT Competition 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

CoRR, 2018

Btor2 , BtorMC and Boolector 3.0.

Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Solving Quantified Bit-Vectors Using Invertibility Conditions.

Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017

Propagation based local search for bit-precise reasoning.

Aina Niemetz, Mathias Preiner, Armin Biere

Formal Methods Syst. Des., 2017

Counterexample-Guided Model Synthesis.

Mathias Preiner, Aina Niemetz, Armin Biere

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Model-Based API Testing for SMT Solvers.

Aina Niemetz, Mathias Preiner, Armin Biere

Proceedings of the 15th International Workshop on Satisfiability Modulo Theories affiliated with the International Conference on Computer-Aided Verification (CAV 2017), Heidelberg, Germany, July 22, 2017

2016

Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories.

Aina Niemetz, Mathias Preiner, Armin Biere

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015

Better Lemmas with Lambda Extraction.

Mathias Preiner, Aina Niemetz, Armin Biere

Proceedings of the Formal Methods in Computer-Aided Design, 2015

2014

Boolector 2.0.

Aina Niemetz, Mathias Preiner, Armin Biere

J. Satisf. Boolean Model. Comput., 2014

Turbo-charging Lemmas on demand with don't care reasoning.

Aina Niemetz, Mathias Preiner, Armin Biere

Proceedings of the Formal Methods in Computer-Aided Design, 2014

2013

Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures.

Martin Aigner, Armin Biere, Christoph M. Kirsch, Aina Niemetz, Mathias Preiner

Proceedings of the POS-13. Fourth Pragmatics of SAT workshop, 2013

Lemmas on Demand for Lambdas.

Mathias Preiner, Aina Niemetz, Armin Biere

Proceedings of the Second International Workshop on Design and Implementation of Formal Tools and Systems, 2013

2012

Resolution-Based Certificate Extraction for QBF - (Tool Presentation).

Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012