Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/30966
Título: | Verification conditions for single-assignment programs |
Autor(es): | Cruz, Daniela da Frade, M. J. Pinto, Jorge Sousa |
Palavras-chave: | Program verification Deductive verification Single-assignment form |
Data: | 2012 |
Editora: | Association for Computing Machinery |
Resumo(s): | A mechanism for generating verification conditions (VCs) for the iteration-free fragment of an imperative language is fundamental in any deductive program verification system. In this paper we revisit symbolic execution, weakest preconditions, and bounded model checking as VC-generation mechanisms, and propose a uniform presentation of the corresponding sets of VCs, in terms of (logical encodings of) paths in the control-flow graph of a single-assignment form of the program under analysis. This allows us to compare the mechanisms, in particular with respect to the size of the generated formulas. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/30966 |
ISBN: | 978-145-030-857-1 |
DOI: | 10.1145/2245276.2231977 |
Versão da editora: | The original publication is available at http://dl.acm.org |
Arbitragem científica: | yes |
Acesso: | Acesso restrito UMinho |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
2012_SAC_12.pdf Acesso restrito! | Documento principal | 361,95 kB | Adobe PDF | Ver/Abrir |