Aina Niemetz

Publication Activity (10 Years)

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

Top Topics

Modulo Theories

Machine Learning

Top Venues

Publications

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)
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
Invited Talk: Local Search for Bit-Precise Reasoning and Beyond. SMT (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)
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 J. Thomas, Christopher Torng, Leonard Truong, Nestan Tsiskaridze, Keyi Zhang
Creating an Agile Hardware Design Flow. DAC (2020)
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)
Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, Giles Reger
The SMT Competition 2015-2018. J. Satisf. Boolean Model. Comput. 11 (1) (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)