TBFV-SE: Testing-Based Formal Verification with Symbolic Execution
TBFV-SE: Testing-Based Formal Verification with Symbolic Execution
复制标题
TBFV-SE：基于测试的带有符号执行的形式验证
DOI：
10.1109/qrs.2018.00019
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Shaoying Liu
中科院分区：
文献类型：
--
作者：
Rong Wang;Shaoying Liu
基于测试的形式化验证（TBFV）是一种严格的、潜在的自动化方法，用于验证基于规范的测试和Hoare逻辑的遍历程序路径的正确性，但是由于Hoare逻辑可能不适用，它的能力受到限制。为了解决这一挑战，我们提出使用符号执行来取代现有TBFV中的Hoare逻辑，从而增强TBFV的能力。我们将新提出的方法称为TBFV- se （TBFV -符号执行）。与现有的TBFV相比，TBFV- se的优势在于在保留其全自动化特性的同时，适用于广泛的程序。我们描述了TBFV-SE的原理，并给出了两个案例研究来证明其可行性和可用性。我们还讨论了有效使用TBFV-SE的条件以及构建工具支持的潜在挑战。
Testing-Based Formal Verification (TBFV) is a rigorous and potentially automated approach to verifying the correctness of traversed program paths based on specification-based testing and Hoare logic, but its capability is limited due to the fact that Hoare logic may not be applicable. To address this challenge, we propose to use symbolic execution to replace Hoare logic in the existing TBFV, thus enhance the capability of TBFV. We call the newly proposed approach TBFV-SE (TBFV - Symbolic Execution). The advantage of TBFV-SE over the existing TBFV lies in its applicability to wide range of programs while preserving its characteristic of full automation. We descirbe the principle of TBFV-SE and present two case studies to demonstrate its feability and usability. We also discuss the condition under which TBFV-SE can be effectively used and potential challenges in building a tool support.