default search action
Aina Niemetz
Person information
- affiliation: Stanford University, Computer Science Department, CA, USA
- affiliation (Dr.techn., 2017): Johannes Kepler University, Linz, Austria
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Journal Articles
- 2023
- [j8]Haniel Barbosa, Clark W. Barrett
, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz
Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM 66(10): 86-95 (2023) - [j7]Joseph Scott
Algorithm selection for SMT. Int. J. Softw. Tools Technol. Transf. 25(2): 219-239 (2023) - [j6]Joseph Scott
Publisher Correction: Algorithm selection for SMT. Int. J. Softw. Tools Technol. Transf. 25(5): 799-800 (2023) - 2021
- [j5]Aina Niemetz
On solving quantified bit-vector constraints using invertibility conditions. Formal Methods Syst. Des. 57(1): 87-115 (2021) - [j4]Aina Niemetz
Towards Satisfiability Modulo Parametric Bit-vectors. J. Autom. Reason. 65(7): 1001-1025 (2021) - 2019
- [j3]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): 221-259 (2019) - 2017
- [j2]Aina Niemetz
Propagation based local search for bit-precise reasoning. Formal Methods Syst. Des. 51(3): 608-636 (2017) - 2014
- [j1]Aina Niemetz, Mathias Preiner
Boolector 2.0. J. Satisf. Boolean Model. Comput. 9(1): 53-58 (2014)
Conference and Workshop Papers
- 2024
- [c30]Aina Niemetz
Scalable Bit-Blasting with Abstractions. CAV (1) 2024: 178-200 - [c29]Clark W. Barrett
Satisfiability Modulo Theories: A Beginner's Tutorial. FM (2) 2024: 571-596 - 2023
- [c28]Aina Niemetz
Bitwuzla. CAV (2) 2023: 3-17 - [c27]Katalin Fazekas
IPASIR-UP: User Propagators for CDCL. SAT 2023: 8:1-8:13 - 2022
- [c26]Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz
Flexible Proof Production in an Industrial-Strength SMT Solver. IJCAR 2022: 15-35 - [c25]Aina Niemetz
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. CAV (2) 2022: 92-106 - [c24]Andres Nötzli, Haniel Barbosa, Aina Niemetz
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. FMCAD 2022: 65-74 - [c23]Aina Niemetz:
Invited Talk: Local Search for Bit-Precise Reasoning and Beyond. SMT 2022: 1 - [c22]Haniel Barbosa
cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS (1) 2022: 415-442 - [c21]Yoni Zohar
Bit-Precise Reasoning via Int-Blasting. VMCAI 2022: 496-518 - 2021
- [c20]Gereon Kremer
ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends. CAV (2) 2021: 231-242 - [c19]Aina Niemetz
Syntax-Guided Quantifier Instantiation. TACAS (2) 2021: 145-163 - [c18]Joseph Scott
MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers. TACAS (2) 2021: 303-325 - 2020
- [c17]Rick Bahr, Clark W. Barrett, Nikhil Bhagdikar, Alex Carsello, Ross Daly, Caleb Donovick
Creating an Agile Hardware Design Flow. DAC 2020: 1-6 - [c16]Aina Niemetz
Ternary Propagation-Based Local Search for more Bit-Precise Reasoning. FMCAD 2020: 214-224 - [c15]Joseph Scott, Aina Niemetz, Mathias Preiner, Vijay Ganesh:
Abstract: MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers. SMT 2020: 62 - 2019
- [c14]Aina Niemetz
Towards Bit-Width-Independent Proofs in SMT Solvers. CADE 2019: 366-384 - [c13]Martin Brain
Invertibility Conditions for Floating-Point Formulas. CAV (2) 2019: 116-136 - [c12]Andres Nötzli
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. SAT 2019: 279-297 - [c11]Alex Ozdemir
DRAT-based Bit-Vector Proofs in CVC4. SAT 2019: 298-305 - 2018
- [c10]Aina Niemetz
Solving Quantified Bit-Vectors Using Invertibility Conditions. CAV (2) 2018: 236-255 - [c9]Aina Niemetz
Btor2 , BtorMC and Boolector 3.0. CAV (1) 2018: 587-595 - 2017
- [c8]Aina Niemetz, Mathias Preiner, Armin Biere:
Model-Based API Testing for SMT Solvers. SMT 2017: 3-14 - [c7]Mathias Preiner
Counterexample-Guided Model Synthesis. TACAS (1) 2017: 264-280 - 2016
- [c6]Aina Niemetz
Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories. CAV (1) 2016: 199-217 - 2015
- [c5]Mathias Preiner
Better Lemmas with Lambda Extraction. FMCAD 2015: 128-135 - 2014
- [c4]Aina Niemetz
Turbo-charging Lemmas on demand with don't care reasoning. FMCAD 2014: 179-186 - 2013
- [c3]Mathias Preiner, Aina Niemetz, Armin Biere:
Lemmas on Demand for Lambdas. DIFTS@FMCAD 2013 - [c2]Martin Aigner, Armin Biere, Christoph M. Kirsch, Aina Niemetz
Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures. POS@SAT 2013: 28-40 - 2012
- [c1]Aina Niemetz
Resolution-Based Certificate Extraction for QBF - (Tool Presentation). SAT 2012: 430-435
Editorship
- 2021
- [e1]Alexander Nadel, Aina Niemetz:
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. CEUR Workshop Proceedings 2908, CEUR-WS.org 2021 [contents]
Data and Artifacts
- 2023
- [d4]Katalin Fazekas
Supplementary material of submission "IPASIR-UP: User Propagators for CDCL". Zenodo, 2023 - 2022
- [d3]Aina Niemetz
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers. Zenodo, 2022 - [d2]Joseph Scott
MachSMT: Machine Learning Driven Algorithm Selection for SMT Solvers. Zenodo, 2022 - 2021
- [d1]Aina Niemetz
Syntax-Guided Quantifier Instantiation (TACAS 2021 Artifact). Zenodo, 2021
Informal and Other Publications
- 2024
- [i6]Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett:
Using Normalization to Improve SMT Solver Stability. CoRR abs/2410.22419 (2024) - 2020
- [i5]Aina Niemetz, Mathias Preiner:
Bitwuzla at the SMT-COMP 2020. CoRR abs/2006.01621 (2020) - 2019
- [i4]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Towards Bit-Width-Independent Proofs in SMT Solvers. CoRR abs/1905.10434 (2019) - [i3]Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar, Clark W. Barrett:
DRAT-based Bit-Vector Proofs in CVC4. CoRR abs/1907.00087 (2019) - 2018
- [i2]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
On Solving Quantified Bit-Vectors using Invertibility Conditions. CoRR abs/1804.05025 (2018) - [i1]Clark W. Barrett, Haniel Barbosa
CVC4 at the SMT Competition 2018. CoRR abs/1806.08775 (2018)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-10 21:42 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: