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

Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

https://hal-cea.archives-ouvertes.fr/cea-01834992
Contributor : Léna Le Roy <>
Submitted on : Wednesday, July 11, 2018 - 10:02:57 AM
Last modification on : Wednesday, January 23, 2019 - 2:39:33 PM

Links full text

Identifiers

Collections

CEA | DRT | LIST

Citation

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⟩

Share

Metrics

Record views

55