论文标题
使用插值和K诱导对安全性的正式验证
Formal Verification of Safety Properties Using Interpolation and k-induction
论文作者
论文摘要
该技术报告介绍了使用SAT/SMT求解器的两个符号模型检查算法的实现，即基于基于插值的模型检查和基于K诱导的模型检查。我们还对这两种模型检查算法进行了比较分析。
This technical report presents implementation of two symbolic model checking algorithms that use SAT/SMT Solvers, namely interpolation based model checking and k-induction based model checking. We also do a comparative analysis of these two model checking algorithms.
