@inproceedings{befaa41963b6473d8abe03a220cdcab9,
title = "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.",
keywords = "ACSL, Frama-C, deductive verification, program specification, teaching",
author = "Nikolai Kosmatov and Virgile Prevosto and Julien Signoles",
year = "2013",
month = sep,
day = "27",
doi = "10.1007/978-3-642-38916-0\_10",
language = "English",
isbn = "9783642389153",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "168--177",
booktitle = "Tests and Proofs - 7th International Conference, TAP 2013, Proceedings",
note = "7th International Conference on Tests and Proofs, TAP 2013 ; Conference date: 16-06-2013 Through 20-06-2013",
}