Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/14931
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Faria, José Miguel | - |
dc.contributor.author | Martins, J. | - |
dc.contributor.author | Pinto, Jorge Sousa | - |
dc.date.accessioned | 2011-12-07T14:47:05Z | - |
dc.date.available | 2011-12-07T14:47:05Z | - |
dc.date.issued | 2012 | - |
dc.identifier.isbn | 9783642305979 | por |
dc.identifier.issn | 0302-9743 | por |
dc.identifier.uri | https://hdl.handle.net/1822/14931 | - |
dc.description.abstract | This paper describes a tool-supported method for the formal verification of Ada programs. It presents ATOS, a tool that automati- cally extracts a model in SPIN from an Ada Program, together with a set of properties that state the correctness of the model. ATOS is also capable of extracting properties from user-provided annotations in Ada programs, inspired by the Spark Annotation language. The goal of ATOS is to help in the verification of sequential and concurrent Ada pro- grams based on model checking. The paper introduces the details of the proposed mechanisms, as well as the results of experimental validation, through a case study. | por |
dc.description.sponsorship | Fundação para a Ciência e a Tecnologia (FCT) | por |
dc.language.iso | eng | por |
dc.rights | openAccess | por |
dc.subject | Formal verification | por |
dc.subject | Model cheking | por |
dc.subject | SPIN | por |
dc.subject | Ada programs | por |
dc.title | An approach to model checking Ada programs | por |
dc.type | conferencePaper | - |
dc.peerreviewed | yes | por |
sdum.publicationstatus | published | por |
oaire.citationStartPage | 105 | por |
oaire.citationEndPage | 118 | por |
oaire.citationTitle | Proceedings of Inforum'11 | por |
oaire.citationVolume | 7308 LNCS | por |
dc.identifier.doi | 10.1007/978-3-642-30598-6_8 | por |
sdum.journal | Lecture Notes in Computer Science (including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | por |
sdum.conferencePublication | Proceedings of Inforum'11 | - |
Aparece nas coleções: | HASLab - Artigos em revistas internacionais DI/CCTC - Artigos (papers) |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
INFORUM-11-a.pdf | Documento principal | 204,81 kB | Adobe PDF | Ver/Abrir |