<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>47</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">José Miguel Faria</style></author><author><style face="normal" font="default" size="100%">João Martins</style></author><author><style face="normal" font="default" size="100%">Jorge Sousa Pinto</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">An approach to model checking Ada programs</style></title><secondary-title><style face="normal" font="default" size="100%">Proceedings of the 17th Ada-Europe international conference on Reliable Software Technologies - Ada- Europe</style></secondary-title><tertiary-title><style face="normal" font="default" size="100%">Ada-Europe'12</style></tertiary-title></titles><dates><year><style  face="normal" font="default" size="100%">2012</style></year><pub-dates><date><style  face="normal" font="default" size="100%">June</style></date></pub-dates></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/jsp/files/inforum.pdf</style></url></related-urls></urls><publisher><style face="normal" font="default" size="100%">Springer-Verlag</style></publisher><pub-location><style face="normal" font="default" size="100%">Stockholm, Sweden</style></pub-location><pages><style face="normal" font="default" size="100%">105–118</style></pages><isbn><style face="normal" font="default" size="100%">978-3-642-30597-9</style></isbn><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;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.&lt;/p&gt;
</style></abstract></record></records></xml>