基于KeY的程序分析和验证

夏新凯+陈冬火

摘要：可信性是各安全攸关领域软件的基础要求，例如航空航天飞行器控制软件、核电站控制软件和交通控制管理软件等，基于形式化方法的程序验证和分析是确保软件正确，具有可信性的重要手段。相比软件测试，基于定理证明的程序验证具有语法和语义的严格性，和属性相关的完备性。本文对程序形式化Hoare语义规约和相关的程序逻辑推理规则系统进行了详细的讨论。基于形式化验证平台KeY，采用完全自动化和交互式两种方法，对具有一定规模的，含有循环结构，并且具有实际意义的程序进行验证。研究证明过程的具体证明策略和方法，尤其是关于循环不变式的规约方法；对KeY的证明效率，先进性和局限性进行评估。endprint