Skip to Main content Skip to Navigation
Conference papers

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
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.
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)
Document type :
Conference papers
Complete list of metadata
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 : Thursday, June 3, 2021 - 2:56:02 PM

Links full text

istex

Identifiers

Collections

CEA | DRT | LIST | GS-COMPUTER-SCIENCE

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics