Formal Method Foundation
Formal Method Foundation
Website
csslab-ustc.github.io/courses/theory/index
Slices
Class Notes
Review
知识基础（集合、关系与映射、上下文无关文法、基于结构的归纳法）
命题逻辑（语法、自然演绎系统、构造逻辑、语义系统、可靠性与完备性、可判断性）
布尔可满足性（合取范式、解析与传播、DPLL 算法）
谓词逻辑（语法、自然演绎系统、构造逻辑、语义系统、可靠性与完备性、可判断性）
等式与未解释函数理论（可满足性模理论、等式理论、并查集与等价类、未解释函数）
线性算术（语法、Fourier-Motzkin 消元法、单纯形法、分支定界法）
数据结构理论（比特向量、数组、指针、字符串）
理论组合（Nelson-Oppen、理论凸性、DPLL(T)算法）
符号执行（机器抽象模型、操作语义、简单命令式语言、路径条件、混合执行等）
程序验证（霍尔三元、最弱前条件、验证条件等）
程序合成（基于语法的合成、公理化合成等）
Propositional Logic
Constructive Logic
Predicate Logic
SAT
EUF
LA
Fourier-Motzkin
Simplex
Branch & Bound (ILP)
Bit-Vectors
Arrays
Pointer
Combination
Nelson-Oppen Method