Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis.
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.