一句话：提出首个Java正确性见证验证器JCWIT，借助JBMC检验验证器输出见证的可复现性。
软件验证工具的结果需要独立验证，但已有Java见证验证器多针对违例见证，缺乏正确性见证验证器。本文提出JCWIT，这是首个面向Java程序的正确性见证验证器。JCWIT接收原程序、规约和正确性见证，将见证执行状态中的不变式以断言形式插桩到原程序中，再调用Java有界模型检测器JBMC验证变换后程序，从而检查正确性见证结果是否可复现。作者在SV-COMP ReachSafety基准上评估JCWIT，结果表明其能正确验证Java验证器生成的正确性见证。
Witness validation is a formal verification method to independently verify software verification tool results, with two main categories: violation and correctness witness validators. Validators for violation witnesses in Java include Wit4Java and GWIT, but no dedicated correctness witness validators exist. To address this gap, this paper presents the Java Correctness-Witness Validator (JCWIT), the first tool to validate correctness witnesses in Java programs. JCWIT accepts an original program, a specification, and a correctness witness as inputs. Then, it uses invariants of each witness’s execution state as conditions to be incorporated into the original program in the form of assertions, thus instrumenting it. Next, JCWIT employs an established tool, Java Bounded Model Checker (JBMC), to verify the transformed program, hence examining the reproducibility of correct witness results. We evaluated JCWIT in the SV-COMP ReachSafety benchmark, and the results show that JCWIT can correctly validate the correctness witnesses generated by Java verifiers.
@inproceedings{paperbot8533,
title = {JCWIT: A Correctness-Witness Validator for Java Programs Based on Bounded Model Checking},
author = {Zaiyu Cheng and Tong Wu and Peter Schrammel and Norbert Tihanyi and Eddie B. de Lima Filho and Lucas C. Cordeiro},
booktitle = {ISSTA},
year = {2024},
doi = {10.1145/3650212.3685303}
}