SPARK-BMC : checking SPARK code for bugs

• Author(s): Lourenço, Cláudio ; Miraldo, Victor Cacciari ; Frade, M. J. ; Pinto, Jorge Sousa
• Date: 2013
• Persistent ID: http://hdl.handle.net/1822/26411
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): Program verification; SPARK; Bounded model checking of software
• Document Type: Conference Object
• Language: English

Description

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 the existing tools for SPARK.