形式化验证
用数学方法证明代码正确性
通过前后置条件对输入输出进行形式化描述
不再需要构造单独测试用例
通过模型检查 定理证明等手段
配合SAT/SMT求解器
对 待验证命题 进行严格证明
对被违反的规约性质
通常可以提供完整反例和错误发生路径
测试用例
数学证明
错误反例
无需
严格
严格
提供
云端部署
部署云端
随地登录验证
随时同步验证进度
保障运行时安全
通过抽象解释算法，自动发现漏洞
内存越界读写
指针安全
整型/浮点型算数溢出
类型转换错误
除零错误
内存泄漏
规约分离&C语言
▶ 规约完全采用C语言，使用成本更可控
▶ 提供大量验证函数，使用方便更灵活
▶ 项目验证代码隔离，开发验证不干扰
▶ 规约代码封装复用，验证效率再提高
多线程管理
多线程并发，验证提速
任务可管理，验证提效
|
|
地址：浙江省杭州市余杭区创鑫时代广场2号楼（浙江人才大厦）1001室
邮箱：wangan@wonsec.com
电话：400-675-8118
扫描二维码
关注微信公众号
扫描二维码
关注微信视频号