%0 Conference Paper
%B Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis
%D 2014
%T A Bounded Model Checker for SPARK Programs
%A Cláudio Belo Lourenço
%A Maria João Frade
%A Jorge Sousa Pinto
%C Sydney, Australia
%X <p>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.</p>
%8 November
%> https://haslab.uminho.pt/sites/default/files/claudio/files/tool-paper-atva2014.pdf