Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/35223| Título: | A bounded model checker for SPARK programs |
| Autor(es): | Lourenço, Cláudio Belo Frade, M. J. Pinto, Jorge Sousa |
| Palavras-chave: | Bounded model checking of software SPARK |
| Data: | 2014 |
| Editora: | Springer |
| Revista: | Lecture Notes in Computer Science |
| Citação: | C. B. Lourenço, M. J. Frade, and J. S. Pinto. A Bounded Model Checker for SPARK Programs (tool paper). In Proceedings of Automated Technology for Verification and Analysis - 12th International Symposium (ATVA 2014), volume 8837 of Lecture Notes in Computer Science, pages 24–30, Berlin, Heidelberg, 2014. Springer-Verlag. |
| Resumo(s): | This paper discusses the design and implementation of a bounded model checker for SPARK code, and provides a proof of concept of the utility and practicality of bounded verification for SPARK. |
| Tipo: | Artigo em ata de conferência |
| URI: | https://hdl.handle.net/1822/35223 |
| ISBN: | 978-3-319-11935-9 |
| DOI: | 10.1007/978-3-319-11936-6_3 |
| ISSN: | 0302-9743 |
| Versão da editora: | The original publication is available at www.springerlink.com |
| Arbitragem científica: | yes |
| Acesso: | Acesso aberto |
| Aparece nas coleções: |
Ficheiros deste registo:
| Ficheiro | Descrição | Tamanho | Formato | |
|---|---|---|---|---|
| 2014_ATVA_14.pdf | Documento principal | 317,17 kB | Adobe PDF | Ver/Abrir |
