CAOVerif: an open-source deductive verification platform for cryptographic software implementations

CAO is a domain-specific imperative language for cryptography, offering a rich mathematical type system and crypto-oriented language constructions. We describe the design and implementation of a deductive verification platform for CAO and demonstrate that the development time of such a complex verif...

Full description

Bibliographic Details
Main Author: Almeida, José Bacelar (author)
Other Authors: Barbosa, Manuel (author), Filliâtre, Jean-Christophe (author), Pinto, Jorge Sousa (author), Vieira, Bárbara Isabel Sousa (author)
Format: article
Language:eng
Published: 2014
Subjects:
Formal verification
Program verification
Cryptographic software
Deductive verification
Engenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informática
Ciências Naturais::Ciências da Computação e da Informação
Science & Technology
Online Access:https://hdl.handle.net/1822/31023
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/31023

Internet

https://hdl.handle.net/1822/31023

Similar Items