<?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%">Daniela Cruz</style></author><author><style face="normal" font="default" size="100%">Maria João Frade</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%">Verification conditions for single-assignment programs</style></title><secondary-title><style face="normal" font="default" size="100%">Proceedings of the 27th Annual Symposium on Applied Computing - SAC</style></secondary-title><tertiary-title><style face="normal" font="default" size="100%">SAC '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%">March</style></date></pub-dates></dates><urls><web-urls><url><style face="normal" font="default" size="100%">http://doi.acm.org/10.1145/2245276.2231977</style></url></web-urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/jsp/files/verification-conditions-revised.pdf</style></url></related-urls></urls><publisher><style face="normal" font="default" size="100%">ACM</style></publisher><pub-location><style face="normal" font="default" size="100%">Trento, Italy</style></pub-location><pages><style face="normal" font="default" size="100%">1264–1270</style></pages><isbn><style face="normal" font="default" size="100%">978-1-4503-0857-1</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 is a systematic study of veriﬁcation conditions and their use in the context of program veriﬁcation. We take Hoare logic as a starting point and study in detail how a veriﬁcation conditions generator can be obtained from it. The notion of program annotation is essential in this process. Weakest preconditions and the use of updates are also studied as alternative approaches to veriﬁcation conditions. Our study is carried on in the context of a While language. Important extensions to this language are considered toward the end of the paper. We also brieﬂy survey modern program veriﬁcation tools and their approaches to the generation of veriﬁcation conditions.&lt;/p&gt;
</style></abstract></record></records></xml>