Zobrazeno 1 - 10
of 10
pro vyhledávání: '"Robert Brummayer"'
Publikováno v:
EPiC Series in Computing.
This paper seeks to explore the predictability of SAT and SMT solvers in response to different kinds of changes to benchmarks. We consider both semantics-preserving and possibly semantics-modifying transformations, and provide preliminary data about
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f16ae9c77725bf0ecf7aa6fe3e9b482b
https://doi.org/10.29007/h5vg
https://doi.org/10.29007/h5vg
Autor:
Robert Brummayer, Armin Biere
Publikováno v:
Journal on Satisfiability, Boolean Modeling and Computation. 6:165-201
The quantifier-free extensional theory of arrays TA plays an important role in hardware and software verification. In this article we present a novel decision procedure that refines formula abstractions with lemmas on demand. We consider the case whe
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ba697c50224fc1e1f1c9dac1785930a7
https://doi.org/10.3233/sat190067
https://doi.org/10.3233/sat190067
Autor:
Matti Järvisalo, Robert Brummayer
This paper develops automated testing and debugging techniques for answer set solver development. We describe a flexible grammar-based black-box ASP fuzz testing tool which is able to reveal various defects such as unsound and incomplete behavior, i.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::94f4ff723cd8499091c6d3d59649424a
http://arxiv.org/abs/1007.3223
http://arxiv.org/abs/1007.3223
Publikováno v:
Theory and Applications of Satisfiability Testing – SAT 2010 ISBN: 9783642141850
SAT
SAT
Robustness and correctness are essential criteria for SAT and QBF solvers. We develop automated testing and debugging techniques designed and optimized for SAT and QBF solver development. Our fuzz testing techniques are able to find critical solver d
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::58650dff2c01f4edd594ce40685865d7
https://doi.org/10.1007/978-3-642-14186-7_6
https://doi.org/10.1007/978-3-642-14186-7_6
Autor:
Robert Brummayer, Armin Biere
Publikováno v:
Proceedings of the 7th International Workshop on Satisfiability Modulo Theories.
SMT solvers are widely used as core engines in many applications. Therefore, robustness and correctness are essential criteria. Current testing techniques used by developers of SMT solvers do not satisfy the high demand for correct and robust solvers
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::14a5a9b7d4d478fefb8f8aacf71f5816
https://doi.org/10.1145/1670412.1670413
https://doi.org/10.1145/1670412.1670413
Autor:
Armin Biere, Robert Brummayer
Publikováno v:
Computer Aided Systems Theory-EUROCAST 2009 ISBN: 9783642047718
EUROCAST
EUROCAST
Recently, it has been proposed to use approximation techniques in the context of decision procedures for the quantifier-free theory of fixed-size bit-vectors. We discuss existing and novel variants of under-approximation techniques. Under-approximati
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::462560deca89455f77ecc4b7f53fa5b7
https://doi.org/10.1007/978-3-642-04772-5_40
https://doi.org/10.1007/978-3-642-04772-5_40
Autor:
Robert Brummayer, Armin Biere
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783642007675
TACAS
TACAS
Satisfiability Modulo Theories (SMT) is the problem of deciding satisfiability of a logical formula, expressed in a combination of first-order theories. We present the architecture and selected features of Boolector, which is an efficient SMT solver
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f94367c9f5e761fe6adc596a69b8f6a0
https://doi.org/10.1007/978-3-642-00768-2_16
https://doi.org/10.1007/978-3-642-00768-2_16
Autor:
Robert Brummayer, Armin Biere
Publikováno v:
FMCAD
This paper shows how all different constraints (ADCs) over bit-vectors can be handled within a SAT solver. It also contains encouraging experimental results in applying this technique to encode simple path constraints in bounded model checking. Final
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::44e0fc629ad716e68e0249f70c267f6a
https://doi.org/10.1109/fmcad.2008.ecp.32
https://doi.org/10.1109/fmcad.2008.ecp.32
Publikováno v:
Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning.
This is a proposal for a bit-precise word-level format, called BTOR. It is easy to parse and has precise semantics. In its basic form it allows to model SMT problems over the quantifier-free theory of bit-vectors in combination with one-dimensional a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d22428ab467079e2d9d92b5b98e0164b
https://doi.org/10.1145/1512464.1512472
https://doi.org/10.1145/1512464.1512472
Autor:
Armin Biere, Robert Brummayer
Publikováno v:
Computer Aided Verification ISBN: 9783540733676
CAV
CAV
C32SAT is a tool for checking C expressions. It can check whether a given C expression can be satisfied, is tautological, or always defined according to the ISO C99 standard. C32SAT can be used to detect nonportable expressions where program behavior
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ea8ae5338257ab69ad4581946ceae326
https://doi.org/10.1007/978-3-540-73368-3_33
https://doi.org/10.1007/978-3-540-73368-3_33