Aina Niemetz

Research Scientist, Computer Science
Stanford University

           

Publications
Talks
Tools
Awards

Publications

2020

  Aina Niemetz, Mathias Preiner. Ternary Propagation-Based Local Search for More Bit-Precise Reasoning. FMCAD 2020: 214-224. (2020)
PDF DOI Preprint Artifact Bitwuzla

  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

  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 CVC4

  Aina Niemetz, Mathias Preiner. Bitwuzla at the SMT-COMP 2020. CoRR abs/2006.01621. (2020)
PDF Arxiv Bibtex Bitwuzla

2019

  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

  Aina Niemetz, Mathias Preiner, Armin Biere. Boolector at the SMT competition 2019. SMT 2019. (2019)
PDF Bibtex Boolector

  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

  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

  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

2018

  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, 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

2017

  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. Counterexample-Guided Model Synthesis. TACAS 2017: 264-280. (2017)
PDF DOI Bibtex Artifact Boolector

  Aina Niemetz, Mathias Preiner, Armin Biere. Model-Based API Testing for SMT Solvers. SMT 2017. (2017)
PDF Bibtex 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. Boolector at the SMT competition 2017. FMV Reports Series, Technical Report 17/1. (2017)
PDF Bibtex Boolector

2016

  Aina Niemetz, Mathias Preiner, Armin Biere. Boolector at the SMT competition 2016. FMV Reports Series, Technical Report 16/1. (2016)
PDF Bibtex Boolector

  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 Boolector

2015

  Mathias Preiner, Aina Niemetz, Armin Biere. Better Lemmas with Lambda Extraction. FMCAD 2015: 128-135. (2015)
PDF Bibtex 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, Andreas Fröhlich, Armin Biere. Improving Local Search For Bit-Vector Logics in SMT with Path Propagation. DIFTS 2015. (2015)
PDF Bibtex Artifact Boolector

2014

  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 Boolector

  Aina Niemetz, Mathias Preiner, Armin Biere. Boolector at the SMT competition 2014. FMV Report Series, Technical Report 14/1. (2014)
PDF Bibtex Boolector

  Aina Niemetz, Mathias Preiner, Armin Biere. Boolector 2.0 system description. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 9 (1): 53-58. (2014)
PDF DOI Preprint Bibtex Boolector

2013

  Mathias Preiner, Aina Niemetz, Armin Biere. Lemmas on Demand for Lambdas. DIFTS 2013. (2013)
PDF 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 Bibtex

  Aina Niemetz, Armin Biere. ddSMT: A Delta Debugger for the SMT-LIB v2 Format. SMT 2013. (2013)
PDF Bibtex ddSMT

2012

  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 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