望安形式化建模验证工具
基于形式化方法，全面保障基础软硬件安全
形式化验证是指根据代码的形式规范或属性，是使用数学的方法证明其正确性或非正确性的一种技术手段
高阶的形式逻辑及定理证明引擎
强大的高阶逻辑验证能力支持交互式和自动化证明方式
采用一键式按钮给出形式化证明证据
丰富的形式化建模能力
支持多类形式化建模语言
可根据软硬件系统各类型文档构建对应模型
安全要求
符合标准的安全模型
需求
函数式形式化建模语言
设计
过程式形式化建模语言
源码
源码自动转换
灵活的部署方式
友好的用户交互
支持本地部署，集成VSCode IDE
支持公有云/私有云部署、集成Cloud IDE
支持基于Web浏览器的前端界面
形式化建模验证工具
严格的“数学证明”，确保你的代码万无一失。
联系我们
咨询热线 400-675-8118
预约免费会议
一对一专属客服
扫码获取认证资料