paperbot · PL 论文追踪

全部论文 待读 收藏

P2 TBFV4J: An Automated Testing-Based Formal Verification Tool for Java

TBFV4J：一个基于测试的 Java 程序自动形式验证工具
ISSTA Proceedings of the 34th ACM SIGSOFT International Symposium on Software Testing and Analysis2025匹配度 3/10 · 该论文属于自动测试与形式验证结合的工具工作，与用户关注的“形式化验证”有间接关联，但未涉及 LLM/Agent、静态分析在 ML/Agentic 程序中的应用、浮点程序分析或贝叶斯程序分析，因此并非核心方向。引用 2 inbox
Ai Liu, Yang Liu, Shaoying Liu
程序验证测试、调试与修复
crossref: 2026-09-12

AI 速览

一句话：实现 TBFV4J 工具，将基于规约的测试与形式验证结合，使 Java 程序无需手工推导循环不变式即可自动验证。

基于规约的测试只能揭示程序中的缺陷，无法严格证明程序无错；而形式验证虽能针对规约给出功能正确性的严格证明，却往往需要大量人工专业知识来推导循环不变式，才能完成自动化验证。基于测试的形式验证（TBFV）把基于规约的测试与形式验证结合起来，在无需推导循环不变式的前提下自动验证程序是否满足其规约。本文实现了支持 Java 程序的 TBFV4J 工具：用户只需输入功能场景（functional scenario）和相应的 Java 代码，工具即可自动执行测试与验证流程。

问题
基于规约的测试无法证明程序无缺陷，而传统形式验证为保证自动化往往需要人工推导循环不变式，门槛高、开销大。
方法
采用基于测试的形式验证（TBFV）思路，将基于规约的测试与形式验证集成，并实现面向 Java 的 TBFV4J 工具，由功能场景与 Java 代码自动驱动测试与验证。
评估
摘要未给出量化实验数据，评估以工具实现及通过输入功能场景与 Java 代码自动完成测试与验证的流程演示为主。
原文摘要（Abstract）

To check whether a program meets its specification, specification-based testing can only reveal bugs but cannot strictly prove that there is no bug in programs. Although formal verification can provide a strict proof for the functional correctness of programs with respect to the corresponding specifications, it often requires significant manual expertise to derive loop invariants to complete automated verification. Testing-based formal verification (TBFV) integrates specification-based testing and formal verification to implement automated verification of whether a program satisfies its specification without the need to derive loop invariants. In this paper, we implement the TBFV4J tool, which supports TBFV for Java programs, where the user only needs to input a functional scenario with Java code and it will automatically perform testing and verification.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot9580,
  title = {TBFV4J: An Automated Testing-Based Formal Verification Tool for Java},
  author = {Ai Liu and Yang Liu and Shaoying Liu},
  booktitle = {ISSTA},
  year = {2025},
  doi = {10.1145/3713081.3731740}
}