【关注】望安科技受邀参加2023 CCF中国软件大会，W-AVC和W-Cert工具亮相会场！
来源:
|
作者:望安科技
|
发布时间: 289天前
|
652 次浏览
|
分享到:
12月2日，由中国计算机学会（CCF）主办，CCF系统软件专委会、形式化方法专委会、软件工程专委会、复旦大学承办的2023 CCF中国软件大会(ChinaSoft 2023)在上海国际会议中心正式开幕。
CCF中国软件大会是我国软件领域规模最大、影响力最广的学术会议。本届大会聚焦“智能化软件创新推动数字经济与社会发展”主题，包含学术、工业、教育以及竞赛四大类50余场活动，吸引来自十个国家和地区的高校、科研机构、企事业单位的2300余位专家学者参会交流学术，深度碰撞思想，以期超前谋划，踩准步点，推动我国软件技术与产业发展。
望安科技作为系统形式化验证与安全认证的推动者，受邀参加了本次大会，并由创始人-赵永望做了安全攸关软件形式化验证工具的专题报告，介绍了望安形式化验证工具W-AVC和W-Cert的独特优势。两个工具的亮相在会场引起了热烈的反响和广泛的关注。
望安C代码自动验证平台W-AVC是由望安科技研发的C语⾔代码程序的形式化验证云平台。平台基于形式化验证技术，通过数学证明排查代码中的缺陷和安全隐患；同时通过开发验证⼈员编写的规约基准代码，⾃动检查代码中的安全漏洞，从而在开发流程的早期增强系统的安全性，减少现代⼤型软件架构带来的⻛险。
1.形式化验证：望安W-AVC采用学界领先的形式化验证技术，无需专门设计测试用例，验证通过可百分百确保规约满足性，用数学证明保证无漏洞。
2.云端部署：项目云端验证，支持私有云部署，省去繁琐环境配置工作。随地登录验证，随时同步验证进度，支持私有云等相关定制化服务。
3.C语法规约：规约完全采用C语言语法，无需为消耗额外学习成本，开发测试人员无缝上手。工具提供内存、算术安全相关大量验证函数，使用方便、灵活。
4.规约分离：W-AVC实现了项目源代码与验证代码分离，验证代码不影响源码运行，提升开发/验证管理效率。项目代码区与验证代码区隔离，开发验证互不干扰。规约代码可封装复用，提高验证效率。
5.项目管理：W-AVC支持多项目上传与管理，验证报告显示覆盖率数据和错误追踪日志。平台支持文件创建、删除、修改等基本操作。验证代码区可创建桩函数、验证辅助函数文件，让形式化验证工程化。
6.多线程任务：平台支持证任务并行验证和中断操作，全方位升级验证工程效率。工具提供验证任务的批量验证、筛选、查看、取消等管理功能。
