<?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%">Paulo Sérgio 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%">Deductive verification of cryptographic software</style></title><secondary-title><style face="normal" font="default" size="100%">Innovations in Systems and Software Engineering</style></secondary-title></titles><keywords><keyword><style  face="normal" font="default" size="100%">Cryptographic algorithms</style></keyword><keyword><style  face="normal" font="default" size="100%">Program equivalence</style></keyword><keyword><style  face="normal" font="default" size="100%">Program verification</style></keyword><keyword><style  face="normal" font="default" size="100%">Self-composition</style></keyword></keywords><dates><year><style  face="normal" font="default" size="100%">2010</style></year></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/jsp/files/isse_2010.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%">Springer-Verlag New York, Inc.</style></publisher><pub-location><style face="normal" font="default" size="100%">Secaucus, NJ, USA</style></pub-location><volume><style face="normal" font="default" size="100%">6</style></volume><pages><style face="normal" font="default" size="100%">203–218</style></pages><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;We apply state-of-the art deductive verification tools to check security-relevant properties of cryptographic software, including safety, absence of error propagation, and correctness with respect to reference implementations. We also develop techniques to help us in our task, focusing on methods oriented towards increased levels of automation, in scenarios where there are clear obvious limits to such automation. These techniques allow us to integrate automatic proof tools with an interactive proof assistant, where the latter is used off-line to prove once-and-for-all fundamental lemmas about properties of programs. The techniques developed have independent interest for practical deductive verification in general.&lt;/p&gt;
</style></abstract></record></records></xml>