Gillian, Part II: Real-World Verification for JavaScript and C
Gillian, Part II: Real-World Verification for JavaScript and C
复制标题
Gillian，第二部分：JavaScript 和 C 的真实世界验证
DOI：
10.1007/978-3-030-81688-9_38
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Philippa Gardner
中科院分区：
文献类型：
--
作者：
P. Maksimovic;Sacha;J. Santos;Philippa Gardner
我们介绍了验证的基础上分离逻辑吉莉安，一个多语言平台的符号分析工具，这是参数的目标语言的内存模型的发展。我们的工作开发了一种方法，用于构建Gillian的组合内存模型，从而统一呈现JavaScript和C内存模型。我们验证了AWS Encryption SDK消息报头验证模块的JavaScript和C实现，特别是设计了用于两个验证任务的通用抽象，并在JavaScript中发现了两个错误，在C实现中发现了三个错误。
We introduce verification based on separation logic to Gillian, a multi-language platform for the development of symbolic analysis tools which is parametric on the memory model of the target language. Our work develops a methodology for constructing compositional memory models for Gillian, leading to a unified presentation of the JavaScript and C memory models. We verify the JavaScript and C implementations of the AWS Encryption SDK message header deserialisation module, specifically designing common abstractions used for both verification tasks, and find two bugs in the JavaScript and three bugs in the C implementation.
JaVerT 2.0：JavaScript 的组合符号执行
影响因子：
--
作者：
Fragoso Santos J
通讯作者：
Fragoso Santos J
Gillian，第一部分：用于符号执行的多语言平台
DOI：
10.1145/3385412.3386014
发表时间：
2020
期刊：
--
影响因子：
--
作者：
Fragoso Santos J
通讯作者：
Fragoso Santos J