A lesson on proof of programs with Frama-C. Invited tutorial paper - Archive ouverte HAL Access content directly
Conference Papers Year : 2013

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

(1) , (1) , (1)
1

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
26 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More