TY - GEN
T1 - A lesson on proof of programs with Frama-C. Invited tutorial paper
AU - Kosmatov, Nikolai
AU - Prevosto, Virgile
AU - Signoles, Julien
PY - 2013/9/27
Y1 - 2013/9/27
N2 - 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.
AB - 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.
KW - ACSL
KW - Frama-C
KW - deductive verification
KW - program specification
KW - teaching
UR - https://www.scopus.com/pages/publications/84884511225
U2 - 10.1007/978-3-642-38916-0_10
DO - 10.1007/978-3-642-38916-0_10
M3 - Conference contribution
AN - SCOPUS:84884511225
SN - 9783642389153
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 168
EP - 177
BT - Tests and Proofs - 7th International Conference, TAP 2013, Proceedings
T2 - 7th International Conference on Tests and Proofs, TAP 2013
Y2 - 16 June 2013 through 20 June 2013
ER -