形式化驗(yàn)證是目前已知的確認(rèn)程序正確的最可靠的方法,是安全攸關(guān)領(lǐng)域開發(fā)高可信軟件,保證軟件系統(tǒng)的正確性、安全性和可靠性的必備工具。本公司推出了用于C程序驗(yàn)證的形式化驗(yàn)證工具--科創(chuàng)驗(yàn)證器,和為方便用戶學(xué)習(xí)形式化驗(yàn)證方法與技術(shù)的云學(xué)習(xí)平臺(tái)--科創(chuàng)驗(yàn)證器學(xué)習(xí)版。
科創(chuàng)驗(yàn)證工具采用的是基于演繹推理的形式化驗(yàn)證技術(shù),結(jié)合Hoare邏輯演算,形狀圖邏輯推理,自動(dòng)定理證明等技術(shù),根據(jù)程序員給出的有關(guān)程序功能的形式化描述(規(guī)約),結(jié)合程序代碼進(jìn)行演繹推理,保障通過(guò)驗(yàn)證的程序符合形式化規(guī)約的約束,也就是說(shuō)程序是正確的。