A lesson on proof of programs with Frama-C. Invited tutorial paper

N. Kosmatov (1) , V. Prevosto (1) , J. Signoles (1)

1 DILS - Département Ingénierie Logiciels et Systèmes

To help formal verification tools to make their way into industry, they ought to be more widely used in software engineering classes. This tutorial paper serves this purpose and provides a lesson on formal specification and proof of programs with Frama-C, an open-source platform dedicated to analysis of C programs, and acsl, a specification language for C.

Keywords: ACSL; C programs; Deductive verification; Formal Specification; Formal verification tools; Frama-C; Open-source platforms; Program specification; Software engineering; Specification languages; Specifications; Teaching; C (programming language)

Domains: Computer Science [cs]

N. Kosmatov, V. Prevosto, J. Signoles. A lesson on proof of programs with Frama-C. Invited tutorial paper. Tests and Proofs. TAP 2013. Lecture Notes in Computer Science, Jun 2013, Budapest, Hungary. pp.168-177, ⟨10.1007/978-3-642-38916-0_10⟩. ⟨cea-01834992⟩