Zobrazeno 1 - 10
of 25
pro vyhledávání: '"Aina Niemetz"'
Publikováno v:
International Journal on Software Tools for Technology Transfer. 25:219-239
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::21027ce9f98681e045006caf2c91b7b6
https://doi.org/10.1007/s10009-023-00696-0
https://doi.org/10.1007/s10009-023-00696-0
Publikováno v:
Journal of Automated Reasoning. 65:1001-1025
Many SMT solvers implement efficient SAT-based procedures for solving fixed-size bit-vector formulas. These techniques, however, cannot be used directly to reason about bit-vectors of symbolic bit-width. To address this shortcoming, we propose a tran
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0feba70c9ea7c21161feab14ff8198c3
https://doi.org/10.1007/s10817-021-09598-9
https://doi.org/10.1007/s10817-021-09598-9
Autor:
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
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030995232
cvc5 is the latest SMT solver in the cooperating validity checker series and builds on the successful code base of CVC4. This paper serves as a comprehensive system description of cvc5 ’s architectural design and highlights the major features and c
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ae0418867d7f4ddd7ebc064a0a8bfef9
https://doi.org/10.1007/978-3-030-99524-9_24
https://doi.org/10.1007/978-3-030-99524-9_24
Autor:
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030945824
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::05059eddffab55cc69744b2c8a910d08
https://doi.org/10.1007/978-3-030-94583-1_24
https://doi.org/10.1007/978-3-030-94583-1_24
Publikováno v:
Computer Aided Verification ISBN: 9783031131875
SMT solvers are highly complex pieces of software with performance, robustness, and correctness as key requirements. Complementing traditional testing techniques for these solvers with randomized stress testing has been shown to be quite effective. R
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::05dbafd0a0b2add6ccc7c08924724d46
https://doi.org/10.1007/978-3-031-13188-2_5
https://doi.org/10.1007/978-3-031-13188-2_5
Autor:
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
Publikováno v:
Automated Reasoning ISBN: 9783031107689
Proof production for SMT solvers is paramount to ensure their correctness independently from implementations, which are often prohibitively difficult to verify. Historically, however, SMT proof production has struggled with performance and coverage i
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::60d0f76591123217016b58475f230c8b
https://doi.org/10.1007/978-3-031-10769-6_3
https://doi.org/10.1007/978-3-031-10769-6_3
Publikováno v:
Journal on Satisfiability, Boolean Modeling and Computation. 11:221-259
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0306de7e23a492e34531774a1feb54ea
https://doi.org/10.3233/sat190123
https://doi.org/10.3233/sat190123
Publikováno v:
Formal Methods in System Design.
We present a novel approach for solving quantified bit-vector constraints in Satisfiability Modulo Theories (SMT) based on computing symbolic inverses of bit-vector operators. We derive conditions that precisely characterize when bit-vector constrain
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f0a1cc89d167f183272862fd88277ed0
https://doi.org/10.1007/s10703-020-00359-9
https://doi.org/10.1007/s10703-020-00359-9
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030720124
TACAS (2)
TACAS (2)
This paper presents a novel approach for quantifier instantiation in Satisfiability Modulo Theories (SMT) that leverages syntax-guided synthesis (SyGuS) to choose instantiation terms. It targets quantified constraints over background theories such as
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::48aa7c692b455f68850d14e9d1c6e9cf
https://doi.org/10.1007/978-3-030-72013-1_8
https://doi.org/10.1007/978-3-030-72013-1_8
Autor:
Raj Setaluri, Kathleen Feng, Nestan Tsiskaridze, Taeyoung Kong, Jeff Setter, Aina Niemetz, Christopher Torng, Keyi Zhang, Teguh Hofstee, Ross Daly, Mark Horowitz, Maxwell Strange, Qiaoyi Liu, Ankita Nayak, Rick Bahr, Priyanka Raina, Caleb Donovick, David Durst, Stephen Richardson, Gedeon Nyengele, Fredrik Kjolstad, Kavya Sreedhar, Clark Barrett, Leonard Truong, Pat Hanrahan, Alex Carsello, James J. Thomas, Kayvon Fatahalian, Dillon Huff, Makai Mann, Nikhil Bhagdikar, Jackson Melchert
Publikováno v:
DAC
Although an agile approach is standard for software design, how to properly adapt this method to hardware is still an open question. This work addresses this question while building a system on chip (SoC) with specialized accelerators. Rather than us
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0a4216100de6d7d6654e70948321f1f5
https://doi.org/10.1109/dac18072.2020.9218553
https://doi.org/10.1109/dac18072.2020.9218553