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.
Wed 25 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:30 | Formal Analysis and Symbolic ExecutionResearch Papers / Tool Demonstrations at Aurora C Chair(s): Na Meng Virginia Tech | ||
16:00 25mTalk | Model Checking Guided Incremental Testing for Distributed Systems Research Papers Yu Gao Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Dong Wang Institute of software, Chinese academy of sciences, Wensheng Dou Institute of Software Chinese Academy of Sciences, Wenhan Feng Institute of Software, Chinese Academy of Sciences, Yu Liang Institute of Software Chinese Academy of Sciences, Yuan Feng Wuhan Dameng Database Co., Ltd, Jun Wei Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences DOI | ||
16:25 25mTalk | Identifying Multi-Parameter Constraint Errors in Python Data Science Library API Documentations Research Papers Xiufeng Xu Nanyang Technological University, Fuman Xie University of Queensland, Chenguang Zhu Meta AI, Guangdong Bai University of Queensland, Sarfraz Khurshid University of Texas at Austin, Yi Li Nanyang Technological University DOI Pre-print | ||
16:50 25mTalk | Freesia: Verifying Correctness of TEE Communication with Concurrent Separation Logic Research Papers Fanlang Zeng Zhejiang University, Rui Chang Zhejiang University, Hongjian Liu Zhejiang University, Hangzhou, China DOI | ||
17:15 15mDemonstration | TBFV4J: An Automated Testing-Based Formal Verification Tool for Java Tool Demonstrations | ||
Aurora C is the third room in the Aurora wing.
When facing the main Cosmos Hall, access to the Aurora wing is on the right, close to the side entrance of the hotel.