Information Technology Reference
In-Depth Information
objective is different from many other works focused on memory safety, we would
like to better evaluate our solution with respect to the state-of-the-art tools on
commonly used benchmarks. Since we check only specified properties at runtime,
that will require to write or automatically generate e-acsl annotations related
to memory safety. While runtime assertion checking for such a rich specification
language as e-acsl will likely have a greater overhead compared to these tools
(that do not need to monitor function contracts and variable initialization, or
treat specific memory-related e-acsl constructs), some of the implementation
solutions they used can still be applicable in our context. Future work also
includes further optimizations to minimize the calls to the monitoring library
(e.g. redundant checks or irrelevant monitoring).
References
1. Sullivan, M., Chillarege, R.: Software defects and their impact on system avail-
ability: A study of field failures in operating systems. In: The 1991 International
Symposium on Fault-Tolerant Computing (FTCS 1991), pp. 2-9. IEEE Computer
Society (1991)
2. Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion check-
ing in software development. ACM SIGSOFT Software Engineering Notes 31(3),
25-37 (2006)
3. Turing, A.: Checking a large routine. In: The Conference on High Speed Automatic
Calculating Machines, pp. 67-69 (1949)
4. Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr.
Program. 78(5), 293-303 (2009)
5. Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.:
Frama-C: A program analysis perspective. In: Eleftherakis, G., Hinchey, M., Hol-
combe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233-247. Springer, Heidelberg
(2012)
6. Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static
and dynamic analysis of C programs. In: The 28th Annual ACM Symposium on
Applied Computing (SAC 2013), pp. 1230-1235. ACM (2013)
7. Kosmatov, N., Signoles, J.: A lesson on runtime assertion checking with Frama-C.
In: Bensalem, S., Legay, A. (eds.) RV 2013. LNCS, vol. 8174, Springer, Heidelberg
(2013)
8. Szpankowski, W.: Patricia tries again revisited. J. ACM 37(4), 691-711 (1990)
9. Signoles, J.: E-ACSL: Executable ANSI/ISO C Specification Language (January
10. Baudin, P., Filliatre, J.C., Hubert, T., March´e,C.,Monate,B.,Moy,Y.,Prevosto,
V.: ACSL: ANSI/ISO C Specification Language, v1.6 (April 2013),
11. Baudin, P., Pacalet, A., Raguideau, J., Schoen, D., Williams, N.: CAVEAT: a
tool for software validation. In: The 2002 International Conference on Dependable
Systems and Networks (DSN 2002), p. 537. IEEE Computer Society (2002)
12. Filliˆatre,J.-C,Marche, C.: The why/Krakatoa/Caduceus platform for deduc-
tive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS,
vol. 4590, pp. 173-177. Springer, Heidelberg (2007)
