Show simple item record

dc.contributor.author
Bugariu, Alexandra
dc.contributor.author
Müller, Peter
dc.date.accessioned
2020-02-06T15:47:02Z
dc.date.available
2019-11-04T13:16:58Z
dc.date.available
2019-11-04T15:02:32Z
dc.date.available
2020-02-05T20:56:19Z
dc.date.available
2020-02-06T15:47:02Z
dc.date.issued
2019-11-04
dc.identifier.uri
http://hdl.handle.net/20.500.11850/375243
dc.identifier.doi
10.3929/ethz-b-000375243
dc.description.abstract
SMT solvers are at the basis of many applications, such as program verification, program synthesis, and test case generation. For all these applications to provide reliable results, SMT solvers must answer queries correctly. However, since they are complex, highly-optimized software systems, ensuring their correctness is challenging. In particular, state-of-the-art testing techniques do not reliably detect when an SMT solver is unsound. In this paper, we present an automatic approach for generating test cases that reveal soundness errors in the implementations of string solvers, as well as potential completeness and performance issues. We synthesize input formulas that are satisfiable or unsatisfiable by construction and use this ground truth as test oracle. We automatically apply satisfiability-preserving transformations to generate increasingly-complex formulas, which allows us to detect many errors with simple inputs and, thus, facilitates debugging. The experimental evaluation shows that our technique effectively reveals bugs in the implementation of widely-used SMT solvers and applies also to other types of solvers, such as model-counting constraint solvers. We focus on strings here, but our approach carries over to other theories and their combinations.
en_US
dc.format
application/pdf
en_US
dc.language.iso
en
en_US
dc.publisher
Department of Computer Science, ETH Zurich
en_US
dc.rights.uri
http://rightsstatements.org/page/InC-NC/1.0/
dc.subject
automatic testing
en_US
dc.subject
soundness testing
en_US
dc.subject
string solvers
en_US
dc.subject
SMT solvers
en_US
dc.title
Automatically Testing String Solvers
en_US
dc.type
Working Paper
dc.rights.license
In Copyright - Non-Commercial Use Permitted
ethz.size
13 p.
en_US
ethz.publication.place
Zurich
en_US
ethz.publication.status
published
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02664 - Inst. f. Programmiersprachen u. -systeme / Inst. Programming Languages and Systems::03653 - Müller, Peter / Müller, Peter
en_US
ethz.leitzahl.certified
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02664 - Inst. f. Programmiersprachen u. -systeme / Inst. Programming Languages and Systems::03653 - Müller, Peter / Müller, Peter
en_US
ethz.relation.isPreviousVersionOf
10.3929/ethz-b-000397450
ethz.date.deposited
2019-11-04T13:17:06Z
ethz.source
FORM
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2019-11-04T15:02:42Z
ethz.rosetta.lastUpdated
2020-02-06T15:47:13Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Automatically%20Testing%20String%20Solvers&rft.date=2019-11-04&rft.au=Bugariu,%20Alexandra&M%C3%BCller,%20Peter&rft.genre=preprint&rft.btitle=Automatically%20Testing%20String%20Solvers
 Search print copy at ETH Library

Files in this item

Thumbnail

Publication type

Show simple item record