论文标题
吉莉安：所有人的构图符号执行
Gillian: Compositional Symbolic Execution for All
论文作者
论文摘要
我们提出了Gillian，这是一个独立于语言的框架，用于开发组成符号分析工具。 Gillian支持分析的三种口味：全程符号测试，完整验证和Bi-Abduction。它带有完全参数元理论结果和模块化实现，旨在最大程度地减少用户所需的实例化工作。我们通过将Gillian实例化为JavaScript和C来评估Gillian，并对一组数据结构库进行分析，从而获得结果，表明Gillian足够强大，可以推理现实世界中的编程语言。
We present Gillian, a language-independent framework for the development of compositional symbolic analysis tools. Gillian supports three flavours of analysis: whole-program symbolic testing, full verification, and bi-abduction. It comes with fully parametric meta-theoretical results and a modular implementation, designed to minimise the instantiation effort required of the user. We evaluate Gillian by instantiating it to JavaScript and C, and perform its analyses on a set of data-structure libraries, obtaining results that indicate that Gillian is robust enough to reason about real-world programming languages.
