摘要："实践是检验真理的唯一标准",很多软件、系统在开发时都会进行模拟验证,以确保顺利运行。然而近些年来,模拟验证的短板逐渐凸显--伴随着计算机的飞速发展,越来越多超大规模设计出现,对于这些设计来说,仿真挑战过于耗费时间,从理论上进行测试反而更为合适。这种测试被称为"形式化验证",是一种穷尽式数学技术,其原理是利用数学和逻辑的方法来证明计算机系统的正确性。

关键词：形式化验证 计算机系统 上海交通大学 工程学院 电子信息 

单位：不详