軟件形式化驗證專題前言
作者：賀飛; 張立軍 清華大學軟件學院; 北京100084; 北京信息科學與技術國家研究中心; 北京100084; 信息系統安全教育部重點實驗室; 北京100084; 中國科學院軟件研究所; 北京100190; 廣州智能軟件產業研究院; 廣東廣州511458
摘要：形式化方法是建立在邏輯演算、形式語言、自動機理論、程序語義、類型系統等理論基礎之上,對計算系統進行描述和分析的一系列符號與技術的集合。形式化方法可指導軟/硬件系統的規約、設計和驗證,是改善和確保計算系統質量的重要方法。歷史上,形式化方法在硬件和協議驗證方面取得巨大成功。
注：因版權方要求，不能公開全文，如需全文，請咨詢雜志社
