<?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%">Jorge Sousa Pinto</style></author><author><style face="normal" font="default" size="100%">Eduardo Brito</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">Program verification in SPARK and ACSL: a comparative case study</style></title><secondary-title><style face="normal" font="default" size="100%">15th International Conference on Reliable Software Technologies - ADA- Europe</style></secondary-title></titles><dates><year><style  face="normal" font="default" size="100%">2010</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/2010_rstae_10.pdf</style></url></related-urls></urls><pub-location><style face="normal" font="default" size="100%">Valencia, Spain</style></pub-location><abstract><style face="normal" font="default" size="100%">&lt;p&gt;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.&lt;/p&gt;
</style></abstract></record></records></xml>