@conference {PintoJS:dedvcsforvklibc,
	title = {Formal Verification of kLIBC with the WP Frama-C plug-in},
	booktitle = {Proceedings of the 6th NASA Formal Methods Symposium },
	series = {Lecture Notes in Computer Science},
	year = {2014},
	month = {April},
	publisher = {Springer-Verlag},
	organization = {Springer-Verlag},
	address = {Houston, Texas},
	abstract = {<p>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 func- tions from  and . We discuss difficulties encoun- tered and describe in detail a problem in the implementation of common  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 verifica- tion, which cannot be attained by focusing on deep properties of cleaner code, written specifically to be verified.</p>
},
	attachments = {https://haslab.uminho.pt/sites/default/files/jsp/files/2014_nfm_14_a.pdf},
	author = {N. Carvalho and Cristiano da Silva Sousa and Jorge Sousa Pinto and Aaron Tomb}
}