SPARK-BMC: checking SPARK code for bugs

The standard SPARK deductive verification tools, based on contracts, are not practical in early stages when the idea is only bug catching. We discuss the implementation of a bounded model checker for SPARK, focusing on specific challenges of this language. Our tool is fully automatic, complementing...

Full description

Bibliographic Details
Main Author: Lourenço, Cláudio (author)
Other Authors: Miraldo, Victor Cacciari (author), Frade, M. J. (author), Pinto, Jorge Sousa (author)
Format: conferenceObject
Language:eng
Published: 2013
Subjects:
Program verification
SPARK
Bounded model checking of software
Online Access:http://hdl.handle.net/1822/26411
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/26411

Internet

http://hdl.handle.net/1822/26411

Similar Items