Please use this identifier to cite or link to this item:

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
Issue date2014
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
Publisher versionThe original publication is available at
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