%0 Conference Paper
%B Proceedings of the 17th Ada-Europe international conference on Reliable Software Technologies - Ada- Europe
%D 2012
%T An approach to model checking Ada programs
%A José Miguel Faria
%A João Martins
%A Jorge Sousa Pinto
%C Stockholm, Sweden
%I Springer-Verlag
%P 105–118
%R 10.1007/978-3-642-30598-6_8
%S Ada-Europe'12
%X <p>This paper describes a tool-supported method for the formal verication of Ada programs. It presents ATOS, a tool that automatically extracts a model in SPIN from an Ada Program, together with a set of properties that state the correctness of the model. ATOS is also capable of extracting properties from user-provided annotations in Ada programs, inspired by the Spark Annotation language. The goal of ATOS is to help in the verication of sequential and concurrent Ada programs based on model checking. The paper introduces the details of the proposed mechanisms, as well as the results of experimental validation, through a case study.</p>
%8 June
%@ 978-3-642-30597-9
%> https://haslab.uminho.pt/sites/default/files/jsp/files/inforum.pdf