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

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

W-AVC 简介

 W-AVC（Wonsec - Automatic Verifier for C）是一款基于霍尔逻辑的自动化验证C文件的形式化验证工具软件。它采用插件集成的方式，对C语言源代码文件进行形式化验证。

工具通过接收一个包含形式规约语言注释的程序，找到源代码中不符合注释描述的内容，从而确保源代码的功能正确性。该工具提供了用于描述功能的形式规约语言，基于形式规约语言注释的源代码形式化自动验证器，以及良好的验证状态、验证结果与源代码功能错误定位的界面展示。 

快速检测源代码设计与验证描述是否一致，增强代码可靠性

快速达到验证全覆盖,验证后可确保百分百无漏洞

耗时短，万量级代码验证时间在5小时之内

基于霍尔逻辑的自动化验证C文件的形式化验证工具软件。