Please use this identifier to cite or link to this item: https://hdl.handle.net/1822/35223

TitleA bounded model checker for SPARK programs
Author(s)Lourenço, Cláudio Belo
Frade, M. J.
Pinto, Jorge Sousa
KeywordsBounded model checking of software
SPARK
Issue date2014
PublisherSpringer
JournalLecture Notes in Computer Science
CitationC. 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.
Abstract(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.
TypeConference paper
URIhttps://hdl.handle.net/1822/35223
ISBN978-3-319-11935-9
DOI10.1007/978-3-319-11936-6_3
ISSN0302-9743
Publisher versionThe original publication is available at www.springerlink.com
Peer-Reviewedyes
AccessOpen access
Appears in Collections:HASLab - Artigos em atas de conferências internacionais (texto completo)

Files in This Item:
File Description SizeFormat 
2014_ATVA_14.pdfDocumento principal317,17 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID