Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/12651
Título: | Program verification in SPARK and ACSL : a comparative case study |
Autor(es): | Brito, Eduardo Pinto, Jorge Sousa |
Palavras-chave: | Verification ACSL SPARK |
Data: | 2010 |
Editora: | Springer |
Revista: | Lecture Notes in Computer Science |
Resumo(s): | We present a case-study of developing a simple software module using contracts, and rigorously verifying it for safety and functional correctness using two very different programming languages, that share the fact that both are extensively used in safety-critical development: SPARK and C/ACSL. This case-study, together with other investigations not detailed here, allows us to establish a comparison in terms of specification effort and degree of automation obtained with each toolset. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/12651 |
ISBN: | 9783642135491 |
DOI: | 10.1007/978-3-642-13550-7_7 |
ISSN: | 0302-9743 |
Versão da editora: | http://www.springerlink.com/content/k287r16l7v745535/ |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | HASLab - Artigos em revistas internacionais DI/CCTC - Artigos (papers) |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
main.pdf | Documento principal | 162,8 kB | Adobe PDF | Ver/Abrir |