面向 Frama-C 的引理函数：将 C 程序作为证明
软件工程
2018-11-15 v1 计算机科学中的逻辑
摘要
本文描述了在 Frama-C 框架中开发的一种自动主动验证技术。我们概述了引理函数方法，并给出了相应的 ACSL 扩展、其在 Frama-C 中的实现，以及对来自 Linux 内核的一组字符串操作函数的评估。与基于 Coq 等交互式证明器的方法相比，我们阐明了所提方法在证明引理所需工作量方面可带来的益处。讨论了该方法及其实现的当前局限性。
引用
@article{arxiv.1811.05879,
title = {Lemma Functions for Frama-C: C Programs as Proofs},
author = {Grigoriy Volkov and Mikhail Mandrykin and Denis Efremov},
journal= {arXiv preprint arXiv:1811.05879},
year = {2018}
}
备注
8 pages, 2 tables, 7 listings. To appear in the "ISPRAS Open 2018" conference proceedings