Symbooglix: A symbolic execution engine for boogie programs
File(s)
Accepted version
Author(s)
Liew, D
Cadar, C
Donaldson, A
Type
Conference Paper
Abstract
We present the design and implementation of Sym-
booglix, a symbolic execution engine for the Boogie intermediate
verification language. Symbooglix aims to find bugs in Boogie
programs efficiently, providing bug-finding capabilities for any
program analysis framework that uses Boogie as a target
language. We discuss the technical challenges associated with
handling Boogie, and describe how we optimised Symbooglix
using a small training set of benchmarks. This empirically-
driven optimisation approach avoids over-fitting Symbooglix to
our benchmarks, enabling a fair comparison with other tools.
We present an evaluation across 3749 Boogie programs generated
from the SV-COMP suite of C programs using the SMACK front-
end, and 579 Boogie programs originating from several OpenCL
and CUDA GPU benchmark suites, translated by the GPUVerify
front-end. Our results show that Symbooglix significantly out-
performs Boogaloo, an existing symbolic execution tool for Boogie,
and is competitive with GPUVerify on benchmarks for which
GPUVerify is highly optimised. While generally less effective than
the Corral and Duality tools on the SV-COMP suite, Symbooglix
is complementary to them in terms of bug-finding ability.
booglix, a symbolic execution engine for the Boogie intermediate
verification language. Symbooglix aims to find bugs in Boogie
programs efficiently, providing bug-finding capabilities for any
program analysis framework that uses Boogie as a target
language. We discuss the technical challenges associated with
handling Boogie, and describe how we optimised Symbooglix
using a small training set of benchmarks. This empirically-
driven optimisation approach avoids over-fitting Symbooglix to
our benchmarks, enabling a fair comparison with other tools.
We present an evaluation across 3749 Boogie programs generated
from the SV-COMP suite of C programs using the SMACK front-
end, and 579 Boogie programs originating from several OpenCL
and CUDA GPU benchmark suites, translated by the GPUVerify
front-end. Our results show that Symbooglix significantly out-
performs Boogaloo, an existing symbolic execution tool for Boogie,
and is competitive with GPUVerify on benchmarks for which
GPUVerify is highly optimised. While generally less effective than
the Corral and Duality tools on the SV-COMP suite, Symbooglix
is complementary to them in terms of bug-finding ability.
Date Issued
2016-07-21
Date Acceptance
2015-12-21
Citation
2016
Publisher
IEEE
Copyright Statement
© 2016 IEEE. This paper has been accepted for publication in IEEE 9th International Conference on Software Testing, Verification and Validation (ICST)
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Identifier
https://ieeexplore.ieee.org/document/7515458
Grant Number
EP/L002795/1
Source
IEEE International Conference on Software Testing, Verification, and Validation
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Engineering, Electrical & Electronic
Computer Science
Engineering
Publication Status
Published
Start Date
2016-04-10
Finish Date
2016-04-15
Coverage Spatial
Chicago, Illinois
Date Publish Online
2016-07-21