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/UVSQ/CNRS

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Runtime Verification - 4th International Conference, RV 2013, Proceedings
Pages	386-399
Number of pages	14
DOIs	https://doi.org/10.1007/978-3-642-40787-1_29
Publication status	Published - 18 Nov 2013
Externally published	Yes
Event	4th International Conference on Runtime Verification, RV 2013 - Rennes, France Duration: 24 Sept 2013 → 27 Sept 2013

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8174 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	4th International Conference on Runtime Verification, RV 2013
Country/Territory	France
City	Rennes
Period	24/09/13 → 27/09/13

Keywords

Frama-C
e-acsl
executable specification
invalid pointers
program monitoring
runtime assertion checking

Access to Document

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

Cite this

Kosmatov, N., & Signoles, J. (2013). A lesson on runtime assertion checking with Frama-C. In Runtime Verification - 4th International Conference, RV 2013, Proceedings (pp. 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. in 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, pp. 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).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this