Sr. Research Scientist, Computer Science
Stanford University
Clark Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar.
Satisfiability Modulo Theories: A Beginner’s Tutorial.
FM: 571-596. (2024)
Distinguished Tutorial Paper Award
PDF DOI Bibtex Artifact cvc5
Aina Niemetz, Mathias Preiner, Yoni Zohar.
Scalable Bit-Blasting with Abstractions.
CAV (1): 178-200. (2024)
PDF DOI Bibtex Artifact Talk Bitwuzla
Haniel Barbosa, 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: 86-95. (2023)
PDF DOI Bibtex cvc5
Aina Niemetz, Mathias Preiner.
Bitwuzla.
CAV (II): 3-17. (2023)
CAV Distinguished Paper Award
PDF DOI Bibtex Artifact Bitwuzla
Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere.
IPASIR-UP: User Propagators for CDCL.
SAT: 8:1–8:13. (2023)
SAT Highlighted Paper
PDF DOI Bibtex Artifact CaDiCaLcvc5
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh.
Algorithm Selection for SMT.
STTT: 219-239. (2023)
PDF DOI Bibtex Artifact MachSMTcvc5
Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Clark Barrett.
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language.
FMCAD: 65-74. (2022)
PDF DOI Bibtex cvc5
Aina Niemetz, Mathias Preiner, Clark Barrett.
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers.
CAV: 92-106. (2022)
PDF DOI Bibtex Artifact Talk Murxla
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 Barrett.
Flexible Proof Production in an Industrial-Strength SMT Solver.
IJCAR: 15-35. (2022)
PDF DOI Bibtex cvc5
Haniel Barbosa, Clark 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: 415-442. (2022)
SCP Best Tool Paper Award
PDF DOI Bibtex Artifact cvc5
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli.
Bit-Precise Reasoning via Int-Blasting.
VMCAI: 496-518. (2022)
PDF DOI Bibtex Artifact cvc5
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, Cesare Tinelli.
Towards Satisfiability Modulo Parametric Bit-Vectors.
JAR 65 (7): 1001-1035. (2021)
PDF DOI Bibtex Artifact CVC4
Gereon Kremer, Aina Niemetz, Mathias Preiner.
ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends.
CAV: 231-242. (2021)
PDF DOI Bibtex Artifact ddSMT
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli.
Syntax-Guided Quantifier Instantiation.
TACAS: 145–163. (2021)
Nominated for the EATCS Best ETAPS Theory Paper Award
PDF DOI Bibtex Artifact CVC4
Joseph Scott, Aina Niemetz, Mathias Preiner, Saeed Nejati, Vijay Ganesh.
MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers.
TACAS: 303–325. (2021)
PDF DOI Bibtex Artifact MachSMT
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli.
On Solving Quantified Bit-Vector Constraints using Invertibility Conditions.
FMSD 57 (1): 87-115. (2021)
PDF DOI Bibtex Artifact CVC4
Aina Niemetz, Mathias Preiner.
Ternary Propagation-Based Local Search for More Bit-Precise Reasoning.
FMCAD 2020: 214-224. (2020)
PDF DOI Bibtex Artifact Talk Bitwuzla Errata
Rick Bahr, Clark 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, Raj Setaluri, Jeff Setter, Kavya Sreedhar, Maxwell Strange, James Thomas, Christopher Torng, Leonard Truong, Nestan Tsiskaridze, Keyi Zhang.
Creating an Agile Hardware Design Flow.
DAC 2020. (2020)
PDF DOI Bibtex
Clark Barrett, Haniel Barbosa, Martin Brain, Ahmed Irfan, Makai Mann, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Amalee Wilson, Yoni Zohar.
CVC4 at the SMT competition 2020.
SMT 2020. (2020)
PDF Bibtex CVC4
Aina Niemetz, Mathias Preiner.
Bitwuzla at the SMT-COMP 2020.
CoRR abs/2006.01621. (2020)
PDF Arxiv Bibtex Bitwuzla
Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, Giles Reger.
The SMT Competition 2015-2018.
Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 11 (1): 221-259. (2019)
PDF DOI Preprint Bibtex SMT-COMP
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, Cesare Tinelli.
Towards Bit-Width-Independent Proofs in SMT Solvers.
CADE 27. (2019)
PDF DOI Arxiv Bibtex CVC4
Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli.
Invertibility Conditions for Floating-Point Formulas.
CAV 2019: 116-136. (2019)
PDF DOI Preprint Extended Version Bibtex Artifact CVC4
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett, Cesare Tinelli.
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers.
SAT 2019: 279-297. (2019)
PDF DOI Bibtex CVC4
Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark Barrett.
DRAT-based Bit-Vector Proofs in CVC4.
SAT 2019: 298-305. (2019)
PDF DOI Arxiv Bibtex CVC4
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2019.
SMT 2019. (2019)
PDF Bibtex Boolector
Clark Barrett, Haniel Barbosa, Martin Brain, Tim King, Makai Mann, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar.
CVC4 at the SMT competition 2019.
SMT 2019. (2019)
PDF Bibtex CVC4
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli.
Solving Quantified Bit-Vectors Using Invertibility Conditions.
CAV 2018: 236-255. (2018)
PDF DOI Preprint Extended Version Bibtex Artifact CVC4
Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere.
Btor2 , BtorMC and Boolector 3.0.
CAV 2018: 587-595. (2018)
PDF DOI Preprint Bibtex Artifact Boolector
Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Andres Nötzli, Mathias Preiner, Clark Barrett, Cesare Tinelli.
Rewrites for SMT Solvers using Syntax-Guided Enumeration (Work in Progress).
SMT 2018. (2018)
PDF Bibtex CVC4
Clark 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)
PDF Arxiv Bibtex CVC4
Aina Niemetz, Mathias Preiner, Armina Biere.
Boolector at the SMT competition 2018.
FMV Reports Series, Technical Report 18/1. (2018)
PDF Bibtex Boolector
Aina Niemetz, Mathias Preiner, Armin Biere.
Propagation based local search for bit-precise reasoning.
Formal Methods in System Design (FMSD) 51 (3): 608-636. (2017)
PDF DOI Preprint Bibtex Artifact Boolector
Aina Niemetz, Mathias Preiner, Armin Biere.
Model-Based API Testing for SMT Solvers.
SMT 2017. (2017)
PDF URL Bibtex Talk Boolector
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2017.
FMV Reports Series, Technical Report 17/1. (2017)
PDF Bibtex Boolector
Mathias Preiner, Aina Niemetz, Armin Biere.
Counterexample-Guided Model Synthesis.
TACAS 2017: 264-280. (2017)
PDF DOI Bibtex Artifact Boolector
Aina Niemetz.
Bit-Precise Reasoning Beyond Bit-Blasting.
Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University Linz. (2017)
PDF Bibtex BoolectorddSMT
Aina Niemetz, Mathias Preiner, Armin Biere.
Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories.
CAV 2016: 199-217. (2016)
PDF DOI Bibtex Artifact Talk Boolector
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2016.
FMV Reports Series, Technical Report 16/1. (2016)
PDF Bibtex Boolector
Mathias Preiner, Aina Niemetz, Armin Biere.
Better Lemmas with Lambda Extraction.
FMCAD 2015: 128-135. (2015)
PDF DOI Bibtex Boolector
Aina Niemetz, Mathias Preiner, Andreas Fröhlich, Armin Biere.
Improving Local Search For Bit-Vector Logics in SMT with Path Propagation.
DIFTS 2015. (2015)
PDF URL Bibtex Artifact Talk Boolector
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2015.
FMV Reports Series, Technical Report 15/1. (2015)
PDF Bibtex Boolector
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector 2.0.
Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 9 (1): 53-58. (2014)
PDF DOI Preprint Bibtex Boolector
Aina Niemetz, Mathias Preiner, Armin Biere.
Turbo-charging Lemmas on Demand with Don’t Care Reasoning.
FMCAD 2014: 179-186. (2014)
PDF DOI Bibtex Artifact Talk Boolector
Aina Niemetz, Mathias Preiner, Armin Biere.
Boolector at the SMT competition 2014.
FMV Report Series, Technical Report 14/1. (2014)
PDF Bibtex Boolector
Mathias Preiner, Aina Niemetz, Armin Biere.
Lemmas on Demand for Lambdas.
DIFTS 2013. (2013)
PDF URL Bibtex Artifact Boolector
Martin Aigner, Armin Biere, Christoph M. Kirsch, Aina Niemetz, Mathias Preiner.
Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures.
POS 2013. (2013)
PDF DOI Bibtex
Aina Niemetz, Armin Biere.
ddSMT: A Delta Debugger for the SMT-LIB v2 Format.
SMT 2013. (2013)
PDF Bibtex Talk ddSMT
Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, Armin Biere.
Resolution-Based Certificate Extraction for QBF - (Tool Presentation).
SAT 2012: 430-435. (2012)
PDF DOI Bibtex Talk QBFcert
Aina Niemetz.
Extracting and Checking Q-Resolution Proofs from a State-Of-The-Art QBF Solver.
Master Thesis, Informatik, Johannes Kepler University. (2012)
PDF Bibtex QBFcert