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

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.