JaVerT 2.0: compositional symbolic execution for JavaScript
JaVerT 2.0: compositional symbolic execution for JavaScript
复制标题
JaVerT 2.0：JavaScript 的组合符号执行
DOI：
10.1145/3290379
复制
发表时间：
2019
影响因子：
--
通讯作者：
Fragoso Santos J
中科院分区：
文献类型：
--
作者：
Fragoso Santos J
我们提出了一种新的，统一的方法来开发组合符号执行工具，弥合了经典符号执行和基于分离逻辑的组合程序推理之间的差距。使用这种方法，我们建立JaVerT 2.0，一个符号分析工具，JavaScript，遵循语言语义，而不简化。JaVerT 2.0支持整个程序的符号测试、验证，并首次支持基于双向溯因的自动组合测试。支撑JaVerT 2.0的元理论是模块化开发的，简化了证明并为实现提供了信息。我们明确的符号执行错误的处理，使我们能够在整个程序的符号测试过程中给开发人员有意义的反馈，并指导双溯执行的资源的推断。我们评估的性能JaVerT 2.0的一些JavaScript数据结构库，证明：我们的整个程序的符号测试的可扩展性;一个国家的最先进的JavaScript验证的改进;和JavaScript的自动组合测试的可行性。
We propose a novel, unified approach to the development of compositional symbolic execution tools, bridging the gap between classical symbolic execution and compositional program reasoning based on separation logic. Using this approach, we build JaVerT 2.0, a symbolic analysis tool for JavaScript that follows the language semantics without simplifications. JaVerT 2.0 supports whole-program symbolic testing, verification, and, for the first time, automatic compositional testing based on bi-abduction. The meta-theory underpinning JaVerT 2.0 is developed modularly, streamlining the proofs and informing the implementation. Our explicit treatment of symbolic execution errors allows us to give meaningful feedback to the developer during whole-program symbolic testing and guides the inference of resource of the bi-abductive execution. We evaluate the performance of JaVerT 2.0 on a number of JavaScript data-structure libraries, demonstrating: the scalability of our whole-program symbolic testing; an improvement over the state-of-the-art in JavaScript verification; and the feasibility of automatic compositional testing for JavaScript.
登录
查看更多内容
用于分析面向对象程序的强属性的案例最优符号执行算法
DOI：
--
发表时间：
2007
期刊：
IEEE International Conference on Software Engineering and Formal Methods
影响因子：
--
作者：
Xianghua Deng;Robby;J. Hatcliff
通讯作者：
J. Hatcliff
类型针对性测试
DOI：
--
发表时间：
2014
期刊：
European Symposium on Programming
影响因子：
--
作者：
Eric L. Seidel;Niki Vazou;Ranjit Jhala
通讯作者：
Ranjit Jhala
DOI：
10.1145/2103656.2103663
发表时间：
2012-01
期刊：
--
影响因子：
--
作者：
Philippa Gardner;S. Maffeis;Gareth Smith
通讯作者：
Philippa Gardner;S. Maffeis;Gareth Smith
使用 SAT 求解器有效查找错误
DOI：
10.1145/1287624.1287653
发表时间：
2007
期刊：
Proceedings of the 2013 International Conference on Principles and Practices of Programming on the Java Platform: Virtual Machines, Languages, and Tools
影响因子：
--
作者：
Julian T Dolby;M. Vaziri;F. Tip
通讯作者：
F. Tip
伽罗瓦变换器和模块化抽象解释器：用于程序分析的可重用元理论
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