Gillian, part i: a multi-language platform for symbolic execution
Gillian, part i: a multi-language platform for symbolic execution
复制标题
Gillian，第一部分：用于符号执行的多语言平台
DOI：
10.1145/3385412.3386014
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Fragoso Santos J
中科院分区：
文献类型：
--
作者：
Fragoso Santos J
我们介绍Gillian，一个为编程语言开发符号分析工具的平台。在这里，我们关注的是Gillian核心的符号执行引擎，它在目标语言的内存模型上是参数化的。我们给出了符号分析的形式化描述，以及紧跟此描述的模块化实现。我们证明了一个参数完备性结果，引入了抽象状态的限制，推广了经典符号执行中使用的路径条件。我们实例化以获得JavaScript和C语言的可信符号测试工具，并使用这些工具来查找真实代码中的错误，从而证明我们的参数化方法的可行性。
We introduce Gillian, a platform for developing symbolic analysis tools for programming languages. Here, we focus on the symbolic execution engine at the heart of Gillian, which is parametric on the memory model of the target language. We give a formal description of the symbolic analysis and a modular implementation that closely follows this description. We prove a parametric soundness result, introducing restriction on abstract states, which generalises path conditions used in classical symbolic execution. We instantiate to obtain trusted symbolic testing tools for JavaScript and C, and use these tools to find bugs in real-world code, thus demonstrating the viability of our parametric approach.
登录
查看更多内容
DOI：
--
发表时间：
2014
期刊：
International Conference on Architectural Support for Programming Languages and Operating Systems
影响因子：
--
作者：
Stefan Bucur;Johannes Kinder;George Candea
通讯作者：
George Candea
影响因子：
1.1
作者：
David Van Horn;M. Might
通讯作者：
M. Might
一元抽象解释器
DOI：
10.1145/2491956.2491979
发表时间：
2013
期刊：
Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Ilya Sergey;Dominique Devriese;M. Might;Jan Midtgaard;David Darais;D. Clarke;Frank Piessens
通讯作者：
Frank Piessens
JaVerT 2.0：JavaScript 的组合符号执行
影响因子：
--
作者：
Fragoso Santos J
通讯作者：
Fragoso Santos J
伽罗瓦变换器和模块化抽象解释器：用于程序分析的可重用元理论
DOI：
10.1145/2814270.2814308
发表时间：
2014
期刊：
Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
影响因子：
--
作者：
David Darais;M. Might;David Van Horn
通讯作者：
David Van Horn