《基于KeY的程序分析和验证》-工学论文，软件工程论文-论文范文参考-科学狗论文网

标题

基于KeY的程序分析和验证

范文

夏新凯+陈冬火

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

随便看

科学优质学术资源、百科知识分享平台，免费提供知识科普、生活经验分享、中外学术论文、各类范文、学术文献、教学资料、学术期刊、会议、报纸、杂志、工具书等各类资源检索、在线阅读和软件app下载服务。