skip to main content
Idioma:
Primo Search
Clear Search Box
Search in: Busca Geral
Busca Avançada
Busca por Índices

Sound symbolic linking in the presence of preprocessing

Vanspauwen, Gijs ; Jacobs, Bart Merayo, Mercedes G ; Hierons, Robert M ; Bravetti, Mario

Software Engineering and Formal Methods, 11th International Conference, SEFM 2013, Madrid, Spain, September 25-27, 2013. Proceedings, 2013, Vol.8137, p.122-136 [Periódico revisado por pares]

Springer Berlin Heidelberg

Texto completo disponível

Citações Citado por
  • Título:
    Sound symbolic linking in the presence of preprocessing
  • Autor: Vanspauwen, Gijs ; Jacobs, Bart
  • Merayo, Mercedes G ; Hierons, Robert M ; Bravetti, Mario
  • É parte de: Software Engineering and Formal Methods, 11th International Conference, SEFM 2013, Madrid, Spain, September 25-27, 2013. Proceedings, 2013, Vol.8137, p.122-136
  • Descrição: Formal verification enables developers to provide safety and security guarantees about their code. A modular verification approach supports the verification of different pieces of an application in separation. We propose symbolic linking as such a modular approach, since it allows to decide whether or not earlier verified source files can be safely linked together (i.e. earlier proven properties remain valid). If an annotation-based verifier for C source code supports both symbolic linking and preprocessing, care must be taken that symbolic linking does not become unsound. The problem is that the result of a header expansion depends upon the defined macros right before expansion. In this paper, we describe how symbolic linking affects the type checking process and why the interaction with preprocessing results in an unsoundness. Moreover, we define a preprocessing technique which ensures soundness by construction and show that the resulting semantics after type checking are equivalent to the standard C semantics. We implemented this preprocessing technique in VeriFast, an annotation-based verifier for C source code that supports symbolic linking, and initial experiments indicate that the modified preprocessor allows most common use cases. To the extent of our knowledge, we are the first to support both modular and sound verification of annotated C source code.
  • Editor: Springer Berlin Heidelberg
  • Idioma: Inglês
Links
Voltar para lista de resultados

  • Realização: ABCD-USP USP   Logos de Redes Sociais: Freepik

Buscando em bases de dados remotas. Favor aguardar.