Abstract

Modern deductive verification tools succeed in automatically proving the great majority of program annotations thanks in particular to constantly evolving SMT solvers they rely on. The remaining proof goals still require interactively created proof scripts. This tool demo paper presents a new solution for an automatic creation of proof scripts in Frama-C/WP, a popular deductive verifier for C programs. The verification engineer defines a proof strategy describing several initial proof steps, from which proof scripts are automatically generated and applied. Our experiments on a large real-life industrial project confirm that the new proof strategy engine strongly facilitates the verification process by automating the creation of proof scripts, thus increasing the potential of industrial applications of deductive verification on large code bases.

In

Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024

Luxembourg, Luxembourg, April 2024, pages 331-339. Springer. ISBN 978-3-031-57246-3.

The final publication will be available in TACAS 2024, DOI: 10.1007/978-3-031-57246-3_18

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