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.