Lecture Content：

Testingand formal methods are two essential approaches to ensuring softwarereliability. Software testing can only reveal defects, it cannot prove theirabsence. Formal methods, grounded in mathematical logic, can rigorously verifythe correctness of software, but their strictness often limits the degree ofautomation. How to combine the strengths of both approaches while mitigatingtheir limitations, in order to achieve automated software verification andvalidation, is an attractive research problem. In this talk, I will introducean advanced software quality assurance technique called Testing-Based FormalVerification (TBFV), which effectively integrates specification-based testingwith formal verification of program correctness. I will outline the fundamentalprinciples, specific techniques, and challenges of TBFV. A key feature of TBFVis its ability to automatically verify the correctness of all program pathsexplored during testing, while also potentially discovering new paths. Thisdual capability supports both software verification and validation. Once widelyadopted, TBFV is expected to significantly reduce testing time and cost,alleviate developers’ workload, and greatly enhance software reliability andquality.

Speaker Introduction:

Ai Liuis an Associate Professor and Ph.D. supervisor at the College of ComputerScience and Technology, Nanjing University of Aeronautics and Astronautics, anda recipient of China’s National Youth Talent Program (Overseas). He receivedhis bachelor’s degree from the School of the Gifted Young at the University ofScience and Technology of China and his Ph.D. from the School of MathematicalSciences at Peking University. He previously served as an Assistant Professorat Hiroshima University in Japan and is currently seconded to the ForeignExperts Affairs Department of the Ministry of Human Resources and SocialSecurity. He is an executive member of the CCF Formal Methods Special Committeeand an academic committee member of the CCF YOCSEF Nanjing Sub-forum. He alsoserves as a young committee member of the Computational Simulation Division ofthe Chinese Society of Aeronautics and Astronautics. His research interestsinclude coalgebraic modeling of component-based systems, trustworthy software,and formal methods. He has received the Excellent Research Award from theSoftware Engineering Group of the Information Processing Society of Japan andhas published more than 20 papers in leading journals and conferences such asIEEE TSE, IEEE TR, JSS, ISSRE, QRS, ICFEM, and TASE.