夏新凱+陳冬火

摘要：可信性是各安全攸關(guān)領(lǐng)域軟件的基礎(chǔ)要求，例如航空航天飛行器控制軟件、核電站控制軟件和交通控制管理軟件等，基于形式化方法的程序驗(yàn)證和分析是確保軟件正確，具有可信性的重要手段。相比軟件測(cè)試，基于定理證明的程序驗(yàn)證具有語(yǔ)法和語(yǔ)義的嚴(yán)格性，和屬性相關(guān)的完備性。本文對(duì)程序形式化Hoare語(yǔ)義規(guī)約和相關(guān)的程序邏輯推理規(guī)則系統(tǒng)進(jìn)行了詳細(xì)的討論?；谛问交?yàn)證平臺(tái)KeY，采用完全自動(dòng)化和交互式兩種方法，對(duì)具有一定規(guī)模的，含有循環(huán)結(jié)構(gòu)，并且具有實(shí)際意義的程序進(jìn)行驗(yàn)證。研究證明過程的具體證明策略和方法，尤其是關(guān)于循環(huán)不變式的規(guī)約方法；對(duì)KeY的證明效率，先進(jìn)性和局限性進(jìn)行評(píng)估。endprint