Please use this identifier to cite or link to this item:
http://repositorio.inesctec.pt/handle/123456789/5023
Title: | Formal Verification of kLIBC with the WP Frama-C Plug-in |
Authors: | Carvalho,N Sousa,CD Jorge Sousa Pinto Tomb,A |
Issue Date: | 2014 |
Abstract: | 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. |
URI: | http://repositorio.inesctec.pt/handle/123456789/5023 http://dx.doi.org/10.1007/978-3-319-06200-6_29 |
metadata.dc.type: | conferenceObject Publication |
Appears in Collections: | HASLab - Articles in International Conferences |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
P-009-HMT.pdf | 435.14 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.