Applied Mathematics Seminar——基于测试的形式验证：理论扩展与应用探索

Abstract：

测试和形式化方法是保障软件可靠性的两种重要手段。软件测试只能发现软件的错误，不能证明软件没有错误；形式化方法可以严格证明软件中是否有错误，但需要的数理知识限制了其自动化实现的程度。基于测试的形式验证（TBFV）是一种通过结合测试与形式化方法来保证程序正确性的同时降低测试成本的自动验证原理，是一种严格的自动的灰盒测试方法。本报告将讨论TBFV的理论扩展与应用探索。

Biography：

刘艾，南京航空航天大学计算机科学与技术学院副教授，国家级青年人才（海外），分别于中国科学技术大学和北京大学获得学士和博士学位，曾任日本广岛大学助理教授。研究方向包括构件化系统的余代数建模、可信软件、形式化方法等。曾获日本情报处理学会软件工程组的卓越研究赏，曾在IEEE TSE、IEEE TR、JSS、ICFEM等期刊或会议上发表过多篇论文。