Symbooglix: A Symbolic Execution Engine for Boogie Programs
Symbooglix: A Symbolic Execution Engine for Boogie Programs
复制标题
Symbooglix：Boogie 程序的符号执行引擎
DOI：
10.1109/icst.2016.11
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Alastair F. Donaldson
中科院分区：
文献类型：
--
作者：
D. Liew;Cristian Cadar;Alastair F. Donaldson
介绍了Boogie中间验证语言的符号执行引擎Symbooglix的设计与实现。Symbooglix旨在有效地查找Boogie程序中的错误，为任何使用Boogie作为目标语言的程序分析框架提供查找错误的功能。我们讨论了与处理Boogie相关的技术挑战，并描述了我们如何使用一组小型基准测试来优化Symbooglix。这种经验驱动的优化方法避免了过度拟合Symbooglix到我们的基准，使与其他工具的公平比较。我们对使用SMACK前端的SV-COMP C程序套件生成的3749个Boogie程序和源自几个OpenCL和CUDA GPU基准套件的579个Boogie程序进行了评估，这些程序由GPU验证前端翻译。我们的研究结果表明，Symbooglix的性能明显优于Boogie现有的符号执行工具Boogaloo，并且在GPUVerify高度优化的基准测试中与GPUVerify竞争。虽然通常不如SV-COMP套件上的Corral和Duality工具有效，但Symbooglix在bug查找能力方面是对它们的补充。
We present the design and implementation of Symbooglix, 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 ourbenchmarks, 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 GPU Verify front-end. Our results show that Symbooglix significantly out-performs Boogaloo, an existing symbolic execution tool for Boogie, and is competitivewith 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.