A lesson on proof of programs with Frama-C. Invited tutorial paper
- Kosmatov, N.
- Prevosto, V.
- Signoles, J.
Publication date
June 2013
DOI Publisher
Springer Science and Business Media LLCAbstract
Conference of 7th International Conference on Tests and Proofs, TAP 2013 ; Conference Date: 16 June 2013 Through 20 June 2013; Conference Code:99450International audienceTo 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
Add to ORKG