This paper presents our results in the formal verification of kLIBC, a minimalistic C library, using the Frama-C/WP tool. We report how we were able to completely verify a significant number of functions from 〈string.h〉 and 〈stdio.h〉. We discuss difficulties encountered and describe in detail a problem in the implementation of common 〈string.h〉 functions, for which we suggest alternative implementations. Our work shows that it is presently already viable to verify low-level C code, with heavy usage of pointers. Although the properties proved tend to be shallower as the code becomes of a lower-level nature, it is our view that this is an important direction towards real-world software verification, which cannot be attained by focusing on deep properties of cleaner code, written specifically to be verified. © 2014 Springer International Publishing.
CITATION STYLE
Carvalho, N., Da Silva Sousa, C., Pinto, J. S., & Tomb, A. (2014). Formal verification of kLIBC with the WP Frama-C plug-in. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8430 LNCS, pp. 343–358). Springer Verlag. https://doi.org/10.1007/978-3-319-06200-6_29
Mendeley helps you to discover research relevant for your work.