%0 Conference Paper
%B 15th International Conference on Reliable Software Technologies - ADA- Europe
%D 2010
%T Program verification in SPARK and ACSL: a comparative case study
%A Jorge Sousa Pinto
%A Eduardo Brito
%C Valencia, Spain
%X <p>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.</p>
%8 June
%> https://haslab.uminho.pt/sites/default/files/jsp/files/2010_rstae_10.pdf