Skip to Main content Skip to Navigation
Conference papers

An optimized memory monitoring for runtime assertion checking of C programs

Abstract : Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. However, monitoring of annotations for pointers and memory locations (such as being valid, initialized, in a particular block, with a particular offset, etc.) is not straightforward and requires systematic instrumentation and monitoring of memory-related operations. This paper describes the runtime memory monitoring library we developed for execution support of e-acsl, executable specification language for C programs offered by the Frama-C platform for analysis of C code. We present the global architecture of our solution as well as various optimizations we realized to make memory monitoring more efficient. Our experiments confirm the benefits of these optimizations and illustrate the bug detection potential of runtime assertion checking with e-acsl.
Document type :
Conference papers
Complete list of metadatas

https://hal-cea.archives-ouvertes.fr/cea-01834990
Contributor : Léna Le Roy <>
Submitted on : Wednesday, July 11, 2018 - 10:02:50 AM
Last modification on : Monday, February 10, 2020 - 6:14:14 PM

Links full text

Identifiers

Collections

CEA | DRT | LIST

Citation

N. Kosmatov, G. Petiot, J. Signoles. An optimized memory monitoring for runtime assertion checking of C programs. Runtime Verification. RV 2013. Lecture Notes in Computer Science, 2013, Rennes, France. pp.167-182, ⟨10.1007/978-3-642-40787-1_10⟩. ⟨cea-01834990⟩

Share

Metrics

Record views

111