TY - GEN
T1 - An optimized memory monitoring for runtime assertion checking of C programs
AU - Kosmatov, Nikolai
AU - Petiot, Guillaume
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. 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.
AB - 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.
KW - Frama-C
KW - e-acsl
KW - executable specification
KW - invalid pointers
KW - memory monitoring
KW - memory-related errors
KW - runtime assertion checking
U2 - 10.1007/978-3-642-40787-1_10
DO - 10.1007/978-3-642-40787-1_10
M3 - Conference contribution
AN - SCOPUS:84887502830
SN - 9783642407864
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 167
EP - 182
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 -