讲座主题：
Testing-Based Formal Verification for Software Quality Assurance and Cost Reduction
主讲人姓名及介绍：
刘少英，日本法政大学教授，IEEE Fellow和英国计算机协会Fellow。主要研究领域包括软件工程，软件开发的形式化工程方法，软件设计方法，程序验证，软件测试，以及智能软件工程环境。曾领导和主持由日本文部科学省，国立信息研究所等日本政府、财团和大企业资助的20多个项目，创立和发展了“软件开发的形式化工程方法”，研制开发SOFL形式化工程开发语言和方法，由 Springer 出版专著一本，编著IEEE CS Press和Springer LNCS系列出版论文集10多本，国际学术期刊和国际会议发表论文200 多篇。
报告摘要：
“Testing”和“Formal Verification”是软件验证和确认的两种重要手段，但它们面临着严峻的挑战。一个新开发的系统总是包含错误，如何以经济有效的方式正式证明程序的正确性仍然是一个挑战。这里我们将简要讨论当前验证和确认方法的特点和挑战，并介绍一种新的方法，即基于测试的正式验证（TBFV）。TBFV是基于规范的正式测试和用于证明程序正确性的霍尔逻辑的适当集成的结果。它是一种严格的灰盒测试方法。TBFV可以自动应用，以保证程序的正确性和高可靠性。
