Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/26411| Título: | SPARK-BMC: checking SPARK code for bugs |
| Autor(es): | Lourenço, Cláudio Miraldo, Victor Cacciari Frade, M. J. Pinto, Jorge Sousa |
| Palavras-chave: | Program verification SPARK Bounded model checking of software |
| Data: | 2013 |
| Editora: | Universidade de Évora |
| Citação: | V. C. Miraldo, M. J. Frade, C. Lourenço, and J. S. Pinto. SPARK-BMC: Checking Spark code for bugs (Comunicação). Universidade de Évora, 2013 |
| Resumo(s): | The standard SPARK deductive verification tools, based on contracts, are not practical in early stages when the idea is only bug catching. We discuss the implementation of a bounded model checker for SPARK, focusing on specific challenges of this language. Our tool is fully automatic, complementing the existing tools for SPARK. |
| Tipo: | Resumo em ata de conferência |
| URI: | https://hdl.handle.net/1822/26411 |
| Arbitragem científica: | yes |
| Acesso: | Acesso aberto |
| Aparece nas coleções: |
Ficheiros deste registo:
| Ficheiro | Descrição | Tamanho | Formato | |
|---|---|---|---|---|
| paper-short-final.pdf | Documento principal | 245,6 kB | Adobe PDF | Ver/Abrir |
