Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Formal Verification of kLIBC with the WP Frama-C Plug-in
verfasst von : Nuno Carvalho, Cristiano da Silva Sousa, Jorge Sousa Pinto, Aaron Tomb
Erschienen in: NASA Formal Methods
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.