Wonsec Automatic Verifier for C

望安C代码自动验证工具

基于形式化方法的C代码自动验证工具
首页 >> 验证平台 >> C代码形式化验证工具

严格的数字证明


确保你的代码万无一失

W-AVC采用学界领先的形式化验证技术，百分百确保代码功能安全性，用数学证明保证无漏洞

规约完全采用C语言语法，无需为学习额外规约语言耗费精力，开发测试人员无缝上手

逻辑保障无漏洞

W-AVC实现了项目源代码与验证代码分离，支持多验证任务并行，通过错误路径追踪便利代码调试，全方位升级验证工程能力，为代码安全提供贴心保障

云端编辑验证

上传项目至云端即可编辑文件和进行验证，省去大量繁琐环境配置工作

沿用C语言语法

全方位升级验证工程能力

⽣成报告中包含代码覆盖率、安全漏洞在内完整验证报告，更利⽤形式化验证技术优势，为每个错误提供反例和路径，助⼒⾼效debug。

为项⽬提供完善管理功能，除⽂件管理外，还包含项⽬验证辅助函数、桩函数定义管理，让代码验证清晰、⾼效、可复⽤。

基于形式化方法，


全面升级你的C代码测试能力

⽆需提供测试⽤例，W-AVC利⽤形式化验证技术，通过代码前后置条件声明，利⽤SAT/SMT算法，⾃动检测包含数组越界、除零错误、指

针错误、算术溢出等安全漏洞以及断⾔不⼀致性的功能漏洞，充分保障代码安全性。

借鉴单元测试，针对程序函数⽣成与源⽂件分离的验证基准⽂件，⽤户使⽤C语⾔编写基准代码，简洁、灵活、易管理。