Lemma Functions for Frama-C: C Programs as Proofs

Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov

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 ext…