Towards Full Proof Automation in Frama-C Using Auto-active Verification - Archive ouverte HAL Access content directly
Conference Papers Year : 2019

Towards Full Proof Automation in Frama-C Using Auto-active Verification

(1) , (2, 3) , (4)
1
2
3
4

Abstract

While deductive verification is increasingly used on real-life code, making it fully automatic remains difficult. The development of powerful SMT solvers has improved the situation, but some proofs still require interactive theorem provers in order to achieve full formal verification. Auto-active verification relies on additional guiding annotations (assertions, ghost code, lemma functions, etc.) and provides an important step towards a greater automation of the proof. However, the support of this methodology often remains partial and depends on the verification tool. This paper presents an experience report on a complete functional verification of several C programs from the literature and real-life code using auto-active verification with the C software analysis platform Frama-C and its deductive verification plugin . The goal is to use automatic solvers to verify properties that are classically verified with interactive provers. Based on our experience, we discuss the benefits of this methodology and the current limitations of the tool, as well as proposals of new features to overcome them.
Not file

Dates and versions

hal-02317055 , version 1 (15-10-2019)

Identifiers

Cite

Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov. Towards Full Proof Automation in Frama-C Using Auto-active Verification. NFM 2019 - 11th Annual NASA Formal Methods Symposium, May 2019, Houston, TX, United States. pp.88-105, ⟨10.1007/978-3-030-20652-9_6⟩. ⟨hal-02317055⟩
67 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More