C代码形式化验证工具

W-AVC

W-AVC(C代码形式化验证)采用插件集成的方式,对C语言源代码文件进行形式化验证。


C代码形式化验证主要可以分为以下几个模块:



验证报告输出模块

验证结果分析模块根据源代码验证模块返回的验证信息进行结果分析处理。

验证报告输出模块以界面方式展示验证结果信息,包含验证代码位置、验证错误信息等,并根据验证结果提供错误代码位置定位功能。

通过接收一个经过解析的包含形式规约语言注释的源代码,根据霍尔逻辑原理对源代码进行验证,找到其中不符合注释描述的内容,从而确保源代码的功能正确性。