Zobrazeno 1 - 10
of 40
pro vyhledávání: '"Niemetz, Aina"'
Autor:
Niemetz, Aina, Preiner, Mathias
In this paper, we present Bitwuzla, our Satisfiability Modulo Theories (SMT) solver for the theories of bit-vectors, floating-points, arrays and uninterpreted functions and their combinations. We discuss selected features and provide details of its c
Externí odkaz:
http://arxiv.org/abs/2006.01621
Many state-of-the-art Satisfiability Modulo Theories (SMT) solvers for the theory of fixed-size bit-vectors employ an approach called bit-blasting, where a given formula is translated into a Boolean satisfiability (SAT) problem and delegated to a SAT
Externí odkaz:
http://arxiv.org/abs/1907.00087
Autor:
Niemetz, Aina, Preiner, Mathias, Reynolds, Andrew, Zohar, Yoni, Barrett, Clark, Tinelli, Cesare
Many SMT solvers implement efficient SAT-based procedures for solving fixed-size bit-vector formulas. These approaches, however, cannot be used directly to reason about bit-vectors of symbolic bit-width. To address this shortcoming, we propose a tran
Externí odkaz:
http://arxiv.org/abs/1905.10434
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
We present a novel approach for solving quantified bit-vector formulas in Satisfiability Modulo Theories (SMT) based on computing symbolic inverses of bit-vector operators. We derive conditions that precisely characterize when bit-vector constraints
Externí odkaz:
http://arxiv.org/abs/1804.05025
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:
Tools and Algorithms for the Construction and Analysis of Systems
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=pmc_________::8ce869c053a0ac02f0c86a6da0ddc256
http://europepmc.org/articles/PMC7984542
http://europepmc.org/articles/PMC7984542
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:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030720124
TACAS (2)
Tools and Algorithms for the Construction and Analysis of Systems
TACAS (2)
Tools and Algorithms for the Construction and Analysis of Systems
In this paper, we present MachSMT, an algorithm selection tool for Satisfiability Modulo Theories (SMT) solvers. MachSMT supports the entirety of the SMT-LIB language. It employs machine learning (ML) methods to construct both empirical hardness mode
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f66e8422eff8dd6576f0d90c1f13499f