1验证条件生成器
闭卷重建验证条件生成器的对象、公式、算例、算法与失败边界。
形式化方法与程序验证 · 小纸条
选一章打印。双面打印（按长边翻页）后沿虚线剪开，每张卡片正面题目、背面答案。
第 1 页 · 正面（题目）
2路径条件与符号执行
闭卷重建路径条件与符号执行的对象、公式、算例、算法与失败边界。
3SAT、SMT与理论组合
闭卷重建SAT、SMT与理论组合的对象、公式、算例、算法与失败边界。
4SMT模型与反例解释
闭卷重建SMT模型与反例解释的对象、公式、算例、算法与失败边界。
5不可满足核与证明证书
闭卷重建不可满足核与证明证书的对象、公式、算例、算法与失败边界。
6量词、触发器与求解不稳定
闭卷重建量词、触发器与求解不稳定的对象、公式、算例、算法与失败边界。
7整数、实数与位向量语义
闭卷重建整数、实数与位向量语义的对象、公式、算例、算法与失败边界。
第 1 页 · 背面（答案）
对象：符号执行以符号输入和路径条件运行程序，每个分支累积约束。；公式：PC_then=PC∧b；PC_else=PC∧¬b。；算例：输入x符号，if x>0后then路径PC:x>0，else为x≤0。；边界：路径数指数爆炸；把不可满足路径继续展开。。
对象：VCG把带注解程序转成纯逻辑义务；全部有效才接受证明。；公式：VC(P,C,Q)=P⇒wp(C,Q)加循环义务。；算例：P:x≥0，C:x:=x+1，Q:x>0，VC为x≥0⇒x+1>0，有效。；边界：生成器漏路径却仍显示绿色；VC与源代码不可反查。。
对象：无效VC的满足模型给抽象反例，需要映射到参数、堆和路径。；公式：SAT(P∧¬Q) gives countermodel。；算例：VC x≥0⇒x>1无效；模型x=0同时满足前件和否定后件。；边界：模型含内部Skolem值却直接展示给学生。。
对象：SAT处理布尔结构，SMT在布尔骨架上加入整数、数组、位向量等理论。；公式：valid(F) iff UNSAT(¬F)。；算例：检查x>2⇒x>0，将否定x>2∧x≤0交SMT，结果不可满足故有效。；边界：unknown当unsat；混用数学整数与位向量。。
对象：含量词SMT常依赖实例化触发器，可能超时或结果对写法敏感。；公式：∀x.P(x)⇒Q(x)需为相关项实例化。；算例：已有P(a)和全称规则，实例化x=a得到Q(a)。；边界：超时后放宽资源就声称性质必真；触发器自循环。。
对象：unsat core定位共同矛盾的命名约束；proof certificate可由小内核独立检查。；公式：Core⊆Constraints 且 UNSAT(Core)。；算例：约束x>0,x<0,y=1中，前两项构成大小2的核，y无关。；边界：把非最小核当根因；求解器崩溃当证明。。
对象：选择数值理论会改变溢出、除法和顺序性质，必须匹配实现。；公式：bv8(255+1)=0，Int(255+1)=256。；算例：断言x+1>x在数学整数中真，在8位x=255时假。；边界：使用Int证明C整数代码；右移和除法语义不一致。。