测试和形式化方法是保障软件可靠性的两种重要手段。软件测试只能发现软件的错误，不能证明软件没有错误；形式化方法可以用数理逻辑知识严格证明软件中是否有错误，但其严格性限制了自动化实现的程度。如何结合两种方法的优势，同时缓解其局限性，以实现自动化的软件验证与确认，是一个极具吸引力的研究课题。在本次演讲中，我将介绍一种名为“基于测试的形式化验证（Testing-Based Formal Verification, TBFV）”的高级软件质量保证方法，该方法有效地将基于规范的测试与程序正确性的形式化验证相结合。我将阐述TBFV的基本原理、具体技术以及面临的挑战。TBFV的特点在于，它能够自动验证测试过程中探索的所有程序路径的正确性，同时还有可能发现新的路径。这种双重作用有助于软件的验证与确认。一旦全面应用，TBFV有望显著减少测试时间和成本，减轻开发人员的工作负担，并大幅提升软件的可靠性和质量。

刘艾，南京航空航天大学计算机科学与技术学院副教授、博导，国家级青年人才（海外），分别于中国科学技术大学少年班学院和北京大学数学科学学院获得学士和博士学位，曾任日本广岛大学助理教授，现借调于人社部外专司，CCF形式化方法专委会执行委员，CCF YOCSEF南京分论坛学术委员，中国航空学会计算与仿真分会青年委员。研究方向包括构件化系统的余代数建模、可信软件、形式化方法等。曾获日本情报处理学会软件工程组的卓越研究赏，在IEEE TSE、IEEE TR、JSS、ISSRE、QRS、ICFEM、TASE等领域知名期刊或会议上发表了20多篇论文。