Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/35224
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Carvalho, Nuno | por |
dc.contributor.author | Sousa, Cristiano da Silva | por |
dc.contributor.author | Pinto, Jorge Sousa | por |
dc.contributor.author | Tomb, Aaron | por |
dc.date.accessioned | 2015-05-20T13:45:38Z | - |
dc.date.available | 2015-05-20T13:45:38Z | - |
dc.date.issued | 2014 | - |
dc.identifier.citation | N. Carvalho, C. S. Sousa, J. S. Pinto, and A. Tomb. Formal Verification of kLIBC with the WP Frama-C plug-in. In Proceedings of the Sixth NASA Formal Methods Symposium (NFM 2014), volume 8430 of Lecture Notes in Computer Science, pages 343–358, Berlin, Heidelberg, 2014. Springer-Verlag. | por |
dc.identifier.isbn | 978-3-319-06199-3 | - |
dc.identifier.issn | 0302-9743 | por |
dc.identifier.uri | https://hdl.handle.net/1822/35224 | - |
dc.description.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. | por |
dc.description.sponsorship | This work is funded by ERDF - European Regional Development Fund through the COMPETE Programme (operational programme for competitiveness) and by National Funds through the FCT - Fundação para a Ciência e a Tecnologia (Portuguese Foundation for Science and Technology) within project FCOMP-01-0124-FEDER-020486. | por |
dc.language.iso | eng | por |
dc.publisher | Springer | por |
dc.rights | openAccess | por |
dc.subject | Deductive Verification | por |
dc.subject | Frama-C | por |
dc.subject | C libraries | por |
dc.title | Formal verification of kLIBC with the WP frama-C plug-in | por |
dc.type | conferencePaper | por |
dc.peerreviewed | yes | por |
dc.relation.publisherversion | The original publication is available at www.springerlink.com | por |
sdum.publicationstatus | published | por |
oaire.citationStartPage | 343 | por |
oaire.citationEndPage | 358 | por |
oaire.citationTitle | Proceedings of the Sixth NASA Formal Methods Symposium (NFM 2014), Lecture Notes in Computer Science | por |
oaire.citationVolume | 8430 | por |
dc.identifier.doi | 10.1007/978-3-319-06200-6_29 | por |
dc.subject.fos | Ciências Naturais::Ciências da Computação e da Informação | por |
dc.subject.fos | Engenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informática | por |
sdum.journal | Lecture Notes in Computer Science (including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | por |
sdum.conferencePublication | Proceedings of the Sixth NASA Formal Methods Symposium (NFM 2014), Lecture Notes in Computer Science | - |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
2014_NFM_14_a.pdf | Documento principal | 435,14 kB | Adobe PDF | Ver/Abrir |