安全C语言程序验证样例
一些常见算法的安全C语言程序通过了科创验证器的验证，这里所列出的是从中选出的作为学习样例的一部分程序。
程序中的标注是我们对程序行为性质的形式化描述。验证器接受经过标注的代码，通过演绎推理生成验证条件，交给约束求解器自动求解，给出程序点的验证结果。
通过验证的程序是正确的，也就是说程序行为满足了用户的期望。
所有样例程序仅供学习之用，可自由下载。用户可以通过 科创验证器学习平台 载入下载的程序样例，体验程序验证的乐趣。
需要注意的是：程序样例的说明中给出的“验证时间”是随机测得的时间，仅作参考。因程序提交验证时验证服务器的负载不同，验证时间也会有所差异。
By Topic
- 简单程序（Simple Programs） [9 examples]
- 一维数组（One-Dimensional Array） [19 examples]
- 二维数组（Two-Dimensional Array） [10 examples]
- 易变数据结构（Mutable Data Structure） [30 examples]
- 字符串（String Processing） [10 examples]
- PL/0 语言实现（PL/0 Programming Language Mini-Compiler） [6 examples]
By Algorithms
- 排序（Sorting） [9 examples]
- 查找（Searching） [3 example]
- 数值计算（Numerical Computing） [5 examples]
By Keywords
- 引理（Lemma） [11 examples]
- 归纳谓词（Inductive Predicate） [5 example]
- 幽灵语句（Ghost Code） [34 example]
- 逻辑变量与逻辑函数（Logic Variable） [13 examples]
- 形状说明（Shape Description） [26 examples]
- 范域词（Quantitative Linguistics） [3 examples]