2018/11/14 by Grigoriy Volkov, Volkov, Grigoriy, Mikhail Mandrykin +3 · 1 citation
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Security and Verification in Computing #Software Engineering (cs.SE) #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1811.05879
openalex publication_date 2018/11/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.