隨著現(xiàn)代社會信息化程度的提高，與計算機相關(guān)的各種系統(tǒng)故障足以造成巨大的經(jīng)濟損失。機械化的定理證明能夠建立更為嚴格的正確性，從而奠定系統(tǒng)的高可信性。本書闡述機械化定理證明的邏輯基礎和關(guān)鍵技術(shù)，分析比較各類主流證明助手的設計特點，重點討論在編譯器驗證領(lǐng)域取得的重要研究成果，并以實例詳述驗證編譯器的開發(fā)和實現(xiàn)。

更多科學出版社服務，請掃碼獲取。