A Bounded Model Checker for SPARK Programs

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

DOI:

10.1007/978-3-319-11936-6_3

PreviewAttachmentSize
tool-paper-atva2014.pdf317.17 KB