<?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é Bacelar Almeida</style></author><author><style face="normal" font="default" size="100%">Manuel Bernardo Barbosa</style></author><author><style face="normal" font="default" size="100%">Jorge Sousa Pinto</style></author><author><style face="normal" font="default" size="100%">Bárbara Vieira</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">Verifying Cryptographic Software Correctness with Respect to Reference Implementations</style></title><secondary-title><style face="normal" font="default" size="100%">Formal Methods for Industrial Critical Systems - FMICS</style></secondary-title><tertiary-title><style face="normal" font="default" size="100%">Lecture Notes in Computer Science</style></tertiary-title></titles><keywords><keyword><style  face="normal" font="default" size="100%">Best paper award</style></keyword></keywords><dates><year><style  face="normal" font="default" size="100%">2009</style></year><pub-dates><date><style  face="normal" font="default" size="100%">November </style></date></pub-dates></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/mbb/files/09fmics.pdf</style></url></related-urls></urls><publisher><style face="normal" font="default" size="100%">Springer</style></publisher><pub-location><style face="normal" font="default" size="100%">Eindhoven, The Netherlands</style></pub-location><volume><style face="normal" font="default" size="100%">5825</style></volume><pages><style face="normal" font="default" size="100%">37-52</style></pages><isbn><style face="normal" font="default" size="100%">978-3-642-04569-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 presents techniques developed to check program equivalences in the context of cryptographic software development, where specifications are typically reference implementations. The techniques allow for the integration of interactive proof techniques (required given the difficulty and generality of the results sought) in a verification infrastructure that is capable of discharging many verification conditions automatically. To this end, the difficult results in the verification process (to be proved interactively) are isolated as a set of lemmas. The fundamental notion of natural invariant is used to link the specification level and the interactive proof construction process.&lt;/p&gt;
</style></abstract></record></records></xml>