A lesson on proof of programs with Frama-C. Invited tutorial paper - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

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

Résumé

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 et versions

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

Identifiants

Citer

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⟩
38 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More