基于插值与时态归纳的安全性质形式化验证
计算机科学中的逻辑
2022-07-05 v1
摘要
本技术报告给出了两种使用 SAT/SMT 求解器的符号模型检测算法的实现，即基于插值的模型检测与基于 k-归纳的模型检测。我们还对这两种模型检测算法做了对比分析。
引用
@article{arxiv.2207.01338,
title = {Formal Verification of Safety Properties Using Interpolation and k-induction},
author = {Tephilla Prince and Atif Abdur Rahman and Sheerazuddin Syed},
journal= {arXiv preprint arXiv:2207.01338},
year = {2022}
}