Lemma Functions for Frama-C: C Programs as Proofs. - Grigoriy Volkov; Mikhail U. Mandrykin; Denis Efremov (CoRR, 2018)