Lemma Functions for Frama-C: C Programs as Proofs
This work addresses the challenge of program verification for C developers, offering a more efficient alternative to interactive methods, though it is incremental in nature.
The paper tackles the problem of verifying C programs by developing an auto-active verification technique called lemma functions in the Frama-C framework, which reduces the effort required to prove lemmas compared to interactive provers like Coq, as evaluated on string-manipulating functions from the Linux kernel.
This paper describes the development of an auto-active verification technique in the Frama-C framework. We outline the lemma functions method and present the corresponding ACSL extension, its implementation in Frama-C, and evaluation on a set of string-manipulating functions from the Linux kernel. We illustrate the benefits our approach can bring concerning the effort required to prove lemmas, compared to the approach based on interactive provers such as Coq. Current limitations of the method and its implementation are discussed.