形式化驗(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ō)程序是正確的。
