Ceagle
欢迎
1.
概览
1.1.
关于
1.2.
系统需求
1.3.
新功能
1.4.
版本介绍
1.5.
最终用户协议
1.6.
如何购买
1.7.
获取帮助
2.
快速开始
2.1.
网页版
2.2.
命令行版
3.
网页版
3.1.
注册、登陆和登出
3.2.
代码的单文件和多文件上传
3.3.
代码的验证
3.4.
代码文件的新建、删除和重命名
3.5.
代码的修改和保存
3.6.
个性化设置
4.
命令行版
4.1.
通用参数
4.2.
编译器参数
4.3.
验证引擎参数
4.4.
SMT引擎参数
4.5.
验证属性参数
5.
基本功能
5.1.
添加约束
5.2.
添加属性
5.2.1.
属性文件
5.2.2.
通用属性
5.2.3.
代码可达性
5.2.4.
assert
5.3.
开始验证
5.4.
验证结果
6.
高级功能
6.1.
学会使用高级功能
6.2.
选择验证引擎
6.2.1.
DFS引擎
6.2.1.1.
抽象精化
6.2.1.2.
组合验证
6.3.
选择约束求解器
6.3.1.
Z3
6.3.2.
dReal
6.3.3.
MathSAT
6.3.4.
CVC4
7.
FAQ
7.1.
开始使用
7.2.
基本功能
7.3.
高级功能
7.4.
其它
8.
附录：错误代码
Powered by
GitBook
Ceagle
网页版
注册、登陆和登出
代码的单文件和多文件上传
代码的验证
代码文件的新建、删除和重命名
代码的修改和保存
个性化设置