@conference {Lourenco2014,
	title = {A Bounded Model Checker for SPARK Programs},
	booktitle = {Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis},
	year = {2014},
	month = {November },
	address = {Sydney, Australia},
	abstract = {<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>
},
	attachments = {https://haslab.uminho.pt/sites/default/files/claudio/files/tool-paper-atva2014.pdf},
	author = {Cl{\'a}udio Belo Louren{\c c}o and Maria Jo{\~a}o Frade and Jorge Sousa Pinto}
}