- Citation:
- Lourenço CB, Frade MJ, Pinto JS.
2014. A Bounded Model Checker for SPARK Programs. Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis.
Date Presented:
November
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.
Citation Key:
Lourenco2014