登陆
注册
工具列表
Tool list
Coq
2020-06-01
128
-
PAR平台中若干软件构件形式化验证技术研究
PAR平台是本团队研制成功的支撑软件形式化和自动化开发的软件平台。该平台充分体现了功能抽象和数据抽象的优越性,使得软件开发变得便捷和可靠,达到这一性能的关键要素是一批可重用软件构件。为保证整个软件平台...
-
基于Coq记录的矩阵形式化方法
矩阵在工程系统中有广泛的应用,矩阵运算的正确性对工程系统的可靠性有重要影响。Coq是一种基于带类型λ演算的功能强大的高阶定理证明器。虽然Coq类型系统能够很好地描述可变大小的动态数据类型,但是对于固定...
-
基于Z3的Coq自动证明策略的设计和实现
形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高;而使用程序...
