<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>17</ref-type><contributors><authors><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 source-level imperative programs</style></title><secondary-title><style face="normal" font="default" size="100%">Computer Science Review</style></secondary-title></titles><keywords><keyword><style  face="normal" font="default" size="100%">Hoare logic</style></keyword><keyword><style  face="normal" font="default" size="100%">Program annotations</style></keyword><keyword><style  face="normal" font="default" size="100%">Program verification</style></keyword><keyword><style  face="normal" font="default" size="100%">Updates</style></keyword><keyword><style  face="normal" font="default" size="100%">Verification conditions</style></keyword><keyword><style  face="normal" font="default" size="100%">Weakest preconditions</style></keyword></keywords><dates><year><style  face="normal" font="default" size="100%">2011</style></year></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/jsp/files/verification-conditions-revised_2.pdf</style></url></related-urls></urls><number><style face="normal" font="default" size="100%">3</style></number><publisher><style face="normal" font="default" size="100%">Elsevier Science Publishers B. V.</style></publisher><pub-location><style face="normal" font="default" size="100%">Amsterdam, The Netherlands, The Netherlands</style></pub-location><volume><style face="normal" font="default" size="100%">5</style></volume><pages><style face="normal" font="default" size="100%">252–277</style></pages><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 verification conditions and their use in the context of program verification. We take Hoare logic as a starting point and study in detail how a verification 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 verification 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 briefly survey modern program verification tools and their approaches to the generation of verification conditions.&lt;/p&gt;
</style></abstract><issue><style face="normal" font="default" size="100%">3</style></issue></record></records></xml>