望安科技受邀参加第五届中国嵌入式技术大会，发表“形式化验证助力汽车软件开发”的演讲

在过去几十年中，伴随着算法研究和工程实践的日臻完善，形式化验证作为对软件安全保障的「终极手段」，在芯片设计、航空航天、轨道交通等领域得到越来越广泛的应用。近年来，随着汽车领域的软件复杂度和重要度的提升和行业标准和开发模式的日趋成熟，形式化验证技术也正在为汽车领域软件开发和验证带来深刻的变革。

望安科技自主开发的C代码自动化验证平台W-AVC，基于形式化验证技术，可以对C代码中常见的运行时错误做自动检查，并对用户编写的函数功能规约进行验证。平台支持对CERT C、CWE等多个安全漏洞数据库的检测，支持对第三方函数做插桩验证。同时，对于分析报告中的漏洞，W-AVC会给出基于完整路径的具体反例，帮助提升调试效率。

针对车领域标准ISO 26262，W-AVC提供包含形式化验证、代码语句覆盖度、数据流分析等在内的多项设计、实现和验证阶段的工具辅助和证据支持。针对AUTOSAR开发标准，W-AVC提供基于接口标准的第三方插桩库，大大减少验证工作的难度和复杂性。结合平台提供的验证任务管理、IDE插件、CI/CD等工程优化方面的功能，W-AVC将助力未来汽车基础软件研发更安全、更高效。