Zobrazeno 1 - 10
of 26
pro vyhledávání: '"NÖTZLI, ANDRES"'
Autor:
Wilson, Amalee, Noetzli, Andres, Reynolds, Andrew, Cook, Byron, Tinelli, Cesare, Barrett, Clark
For many users of Satisfiability Modulo Theories (SMT) solvers, the solver's performance is the main bottleneck in their application. One promising approach for improving performance is to leverage the increasing availability of parallel and cloud co
Externí odkaz:
http://arxiv.org/abs/2306.05854
Autor:
Sheng, Ying, Nötzli, Andres, Reynolds, Andrew, Zohar, Yoni, Dill, David, Grieskamp, Wolfgang, Park, Junkil, Qadeer, Shaz, Barrett, Clark, Tinelli, Cesare
Dynamic arrays, also referred to as vectors, are fundamental data structures used in many programs. Modeling their semantics efficiently is crucial when reasoning about such programs. The theory of arrays is widely supported but is not ideal, because
Externí odkaz:
http://arxiv.org/abs/2205.08095
CVC4Sy is a syntax-guided synthesis (SyGuS) solver based on bounded term enumeration and, for restricted fragments, quantifier elimination. The enumerative strategies are based on encoding term enumeration as an extension of the quantifier-free theor
Externí odkaz:
http://arxiv.org/abs/1907.10175
Autor:
Barrett, Clark, Barbosa, Haniel, Brain, Martin, Ibeling, Duligur, King, Tim, Meng, Paul, Niemetz, Aina, Nötzli, Andres, Preiner, Mathias, Reynolds, Andrew, Tinelli, Cesare
This paper is a description of the CVC4 SMT solver as entered into the 2018 SMT Competition. We only list important differences from the 2017 SMT Competition version of CVC4. For further and more detailed information about CVC4, please refer to the o
Externí odkaz:
http://arxiv.org/abs/1806.08775
Autor:
Nötzli, Andres, Brown, Fraser
Optimizing floating-point arithmetic is vital because it is ubiquitous, costly, and used in compute-heavy workloads. Implementing precise optimizations correctly, however, is difficult, since developers must account for all the esoteric properties of
Externí odkaz:
http://arxiv.org/abs/1603.09290
Autor:
BARBOSA, HANIEL, BARRETT, CLARK, COOK, BYRON, DUTERTRE, BRUNO, KREMER, GEREON, LACHNITT, HANNA, NIEMETZ, AINA, NÖTZLI, ANDRES, OZDEMIR, ALEX, PREINER, MATHIAS, REYNOLDS, ANDREW, TINELLI, CESARE, ZOHAR, YONI
Publikováno v:
Communications of the ACM; Oct2023, Vol. 66 Issue 10, p86-95, 10p, 1 Color Photograph, 1 Black and White Photograph, 2 Diagrams
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Publikováno v:
Automated Reasoning
In text encoding standards such as Unicode, text strings are sequences of code points, each of which can be represented as a natural number. We present a decision procedure for a concatenation-free theory of strings that includes length and a convers
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=pmc_________::b4bf6abd398dd142ec13d62c3c60403a
http://europepmc.org/articles/PMC7324130
http://europepmc.org/articles/PMC7324130
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.