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...

ver descrição completa

Detalhes bibliográficos
Autor principal: Almeida, José Bacelar (author)
Outros Autores: Barbosa, Manuel (author), Filliâtre, Jean-Christophe (author), Pinto, Jorge Sousa (author), Vieira, Bárbara Isabel Sousa (author)
Formato: article
Idioma:eng
Publicado em: 2014
Assuntos:
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
Texto completo:https://hdl.handle.net/1822/31023
País:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/31023

Texto Completo

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

Registos relacionados