A Bounded Model Checker for SPARK Programs
A Bounded Model Checker for SPARK Programs
Date
2014
Authors
Cláudio Belo Lourenço
Maria João Frade
Jorge Sousa Pinto
Journal Title
Journal ISSN
Volume Title
Publisher
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.