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 WP. 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.

In

Proc. of the 11th NASA Formal Methods Symposium (NFM 2019)

Houston, TX, USA, May 2019, LNCS, vol. 11460, pages 88-105. Springer. ISBN 978-3-030-20651-2. To appear.

Final publication available at http://link.springer.com. DOI: 10.1007/978-3-319-77935-5_3.

Paper (Available PDF is the author's final version of the work)