A lesson on runtime assertion checking with Frama-C

Nikolai Kosmatov; Julien Signoles

doi:10.1007/978-3-642-40787-1_29

A lesson on runtime assertion checking with Frama-C

Nikolai Kosmatov
, Julien Signoles

CEA
CEA/UVSQ/CNRS

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

21 Citations (Scopus)

Résumé

Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. This paper provides a lesson on runtime assertion checking with Frama-C, a publicly available toolset for analysis of C programs. We illustrate how a C program can be specified in executable specification language e-acsl and how this specification can be automatically translated into instrumented C code suitable for monitoring and runtime verification of specified properties. We show how various errors can be automatically detected on the instrumented code, including C runtime errors, failures in postconditions, assertions, preconditions of called functions, and memory leaks. Benefits of combining runtime assertion checking with other Frama-C analyzers are illustrated as well.

langue originale	Anglais
titre	Runtime Verification - 4th International Conference, RV 2013, Proceedings
Pages	386-399
Nombre de pages	14
Les DOIs	https://doi.org/10.1007/978-3-642-40787-1_29
état	Publié - 18 nov. 2013
Modification externe	Oui
Evénement	4th International Conference on Runtime Verification, RV 2013 - Rennes, France Durée: 24 sept. 2013 → 27 sept. 2013

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8174 LNCS
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	4th International Conference on Runtime Verification, RV 2013
Pays/Territoire	France
La ville	Rennes
période	24/09/13 → 27/09/13

Accès au document

10.1007/978-3-642-40787-1_29

Contient cette citation

Kosmatov, N., & Signoles, J. (2013). A lesson on runtime assertion checking with Frama-C. Dans Runtime Verification - 4th International Conference, RV 2013, Proceedings (p. 386-399). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 8174 LNCS). https://doi.org/10.1007/978-3-642-40787-1_29

@inproceedings{c6e6ea30cd434a3ea9794f063a236cac,

title = "A lesson on runtime assertion checking with Frama-C",

abstract = "Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. This paper provides a lesson on runtime assertion checking with Frama-C, a publicly available toolset for analysis of C programs. We illustrate how a C program can be specified in executable specification language e-acsl and how this specification can be automatically translated into instrumented C code suitable for monitoring and runtime verification of specified properties. We show how various errors can be automatically detected on the instrumented code, including C runtime errors, failures in postconditions, assertions, preconditions of called functions, and memory leaks. Benefits of combining runtime assertion checking with other Frama-C analyzers are illustrated as well.",

keywords = "Frama-C, e-acsl, executable specification, invalid pointers, program monitoring, runtime assertion checking",

author = "Nikolai Kosmatov and Julien Signoles",

year = "2013",

month = nov,

day = "18",

doi = "10.1007/978-3-642-40787-1\_29",

language = "English",

isbn = "9783642407864",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "386--399",

booktitle = "Runtime Verification - 4th International Conference, RV 2013, Proceedings",

note = "4th International Conference on Runtime Verification, RV 2013 ; Conference date: 24-09-2013 Through 27-09-2013",

}

Kosmatov, N & Signoles, J 2013, A lesson on runtime assertion checking with Frama-C. Dans Runtime Verification - 4th International Conference, RV 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), VOL. 8174 LNCS, p. 386-399, 4th International Conference on Runtime Verification, RV 2013, Rennes, France, 24/09/13. https://doi.org/10.1007/978-3-642-40787-1_29

A lesson on runtime assertion checking with Frama-C. / Kosmatov, Nikolai; Signoles, Julien.
Runtime Verification - 4th International Conference, RV 2013, Proceedings. 2013. p. 386-399 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 8174 LNCS).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

TY - GEN

T1 - A lesson on runtime assertion checking with Frama-C

AU - Kosmatov, Nikolai

AU - Signoles, Julien

PY - 2013/11/18

Y1 - 2013/11/18

N2 - Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. This paper provides a lesson on runtime assertion checking with Frama-C, a publicly available toolset for analysis of C programs. We illustrate how a C program can be specified in executable specification language e-acsl and how this specification can be automatically translated into instrumented C code suitable for monitoring and runtime verification of specified properties. We show how various errors can be automatically detected on the instrumented code, including C runtime errors, failures in postconditions, assertions, preconditions of called functions, and memory leaks. Benefits of combining runtime assertion checking with other Frama-C analyzers are illustrated as well.

AB - Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. This paper provides a lesson on runtime assertion checking with Frama-C, a publicly available toolset for analysis of C programs. We illustrate how a C program can be specified in executable specification language e-acsl and how this specification can be automatically translated into instrumented C code suitable for monitoring and runtime verification of specified properties. We show how various errors can be automatically detected on the instrumented code, including C runtime errors, failures in postconditions, assertions, preconditions of called functions, and memory leaks. Benefits of combining runtime assertion checking with other Frama-C analyzers are illustrated as well.

KW - Frama-C

KW - e-acsl

KW - executable specification

KW - invalid pointers

KW - program monitoring

KW - runtime assertion checking

U2 - 10.1007/978-3-642-40787-1_29

DO - 10.1007/978-3-642-40787-1_29

M3 - Conference contribution

AN - SCOPUS:84887464191

SN - 9783642407864

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 386

EP - 399

BT - Runtime Verification - 4th International Conference, RV 2013, Proceedings

T2 - 4th International Conference on Runtime Verification, RV 2013

Y2 - 24 September 2013 through 27 September 2013

ER -

A lesson on runtime assertion checking with Frama-C

Résumé

Série de publications

Une conférence

Accès au document

Empreinte digitale

Contient cette citation