SPARK-BMC : checking SPARK code for bugs

• Autor(es): Lourenço, Cláudio ; Miraldo, Victor Cacciari ; Frade, M. J. ; Pinto, Jorge Sousa
• Data: 2013
• Identificador Persistente: http://hdl.handle.net/1822/26411
• Origem: RepositóriUM - Universidade do Minho
• Assunto(s): Program verification; SPARK; Bounded model checking of software
• Tipo de Documento: Documento de conferência
• Idioma: Inglês

Descrição

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.