A Bounded Model Checker for SPARK Programs

dc.contributor.author Cláudio Belo Lourenço en
dc.contributor.author Maria João Frade en
dc.contributor.author Jorge Sousa Pinto en
dc.date.accessioned 2017-12-28T10:28:58Z
dc.date.available 2017-12-28T10:28:58Z
dc.date.issued 2014 en
dc.description.abstract 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. en
dc.identifier.uri http://repositorio.inesctec.pt/handle/123456789/5026
dc.identifier.uri http://dx.doi.org/10.1007/978-3-319-11936-6_3 en
dc.language eng en
dc.relation 6180 en
dc.relation 5595 en
dc.relation 5605 en
dc.rights info:eu-repo/semantics/openAccess en
dc.title A Bounded Model Checker for SPARK Programs en
dc.type conferenceObject en
dc.type Publication en
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
P-009-ZAE.pdf
Size:
299.83 KB
Format:
Adobe Portable Document Format
Description: