Program verification in SPARK and ACSL: a comparative case study

Citation:
Pinto JS, Brito E.  2010.  Program verification in SPARK and ACSL: a comparative case study. 15th International Conference on Reliable Software Technologies - ADA- Europe.

Date Presented:

June

Abstract:

We present a case-study of developing a simple software module using contracts, and rigorously verifying it for safety and functional correctness using two very different programming languages, that share the fact that both are extensively used in safety-critical development: SPARK and C/ACSL. This case-study, together with other investigations not detailed here, allows us to establish a comparison in terms of specification effort and degree of automation obtained with each toolset.

Citation Key:

1618

DOI:

10.1007/978-3-642-13550-7_7

PreviewAttachmentSize
2010_rstae_10.pdf162.8 KB