轻量版VeriFast
计算机科学中的逻辑
2017-01-11 v2
摘要
VeriFast 是用于单线程和多线程 C 和 Java 程序的安全性与正确性属性可靠模块化验证的领先研究原型工具。它已被用作探索与验证新颖程序验证技术及工业案例研究的载体；它在若干程序验证竞赛中表现良好；并被独立于作者的多位教师用于教学。然而，迄今为止，虽然 VeriFast 的操作已在多篇出版物中非正式描述，且特定验证技术已经形式化，但关于 VeriFast 如何工作的清晰精确阐述尚未出现。本文中我们首次给出 VeriFast 程序验证方法核心子集的形式化定义与可靠性证明。该阐述旨在既易懂又严谨：文本基于研究生程序验证课程讲义，并由 Coq 中的可执行机器可读定义与机器检查的可靠性证明支持。
引用
@article{arxiv.1507.07697,
title = {Featherweight VeriFast},
author = {Bart Jacobs and Frédéric Vogels and Frank Piessens},
journal= {arXiv preprint arXiv:1507.07697},
year = {2017}
}