A lesson on proof of programs with Frama-C. Invited tutorial paper - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Access content directly
Conference Papers Year : 2013

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.

Dates and versions

cea-01834992 , version 1 (11-07-2018)

Identifiers

Cite

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⟩

Collections

CEA DRT LIST
29 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More