SPARK-BMC: checking SPARK code for bugs - Lourenço, Cláudio (2013)
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.