Verificação formal de uma implementação eficiente de UTF-8
| dc.contributor.advisor | Gualandi, Hugo Musso | |
| dc.contributor.referee1 | Nobrega, Hugo de Holanda Cunha | |
| dc.contributor.referee2 | Santos, Renan Almeida de Miranda | |
| dc.creator | Santiago, Leonardo Ribeiro | |
| dc.date.accessioned | 2026-02-08T23:28:09Z | |
| dc.date.available | 2026-05-16T03:08:58Z | |
| dc.date.issued | 2025-12-11 | |
| dc.description.resumo | O sistema de codificação Unicode é imprescindível para a comunicação global, permitindo que inúmeros idiomas utilizem a mesma representação para serializar todos os caracteres, eliminando a necessidade de conversão. Dentre todos os formatos de codificação definidos pelo consórcio Unicode, certamente o formato ubíquo é o UTF-8, pela sua retrocompatibilidade com ASCII, e capacidade de economizar bytes. Apesar de ser utilizado em mais de 98% das páginas da internet, vários problemas aparecem ao implementar programas de codificação e decodificação de UTF-8 semanticamente corretos, e múltiplas vulnerabilidades estão associadas a aceitar caracteres UTF-8 inválidos erroneamente. Assim, este trabalho utiliza verificação formal através de provadores de teoremas interativos com dois propósitos. Primeiro, será desenvolvido um conjunto de propriedades - a especificação - que são suficientes para afirmar a corretude de um codicador ou decodificador de UTF-8. Com a especificação formalizada, implementamos um codificador e decodificador, mostrando que esses respeitam todas as propriedades necessárias para que estejam corretos. | pt_BR |
| dc.embargo.terms | aberto | pt_BR |
| dc.identifier.uri | http://hdl.handle.net/11422/28389 | |
| dc.language | por | pt_BR |
| dc.publisher | Universidade Federal do Rio de Janeiro | pt_BR |
| dc.publisher.country | Brasil | pt_BR |
| dc.publisher.department | Instituto de Computação | pt_BR |
| dc.publisher.initials | UFRJ | pt_BR |
| dc.rights | Acesso Aberto | pt_BR |
| dc.subject | Verificação formal | pt_BR |
| dc.subject | Software correto | pt_BR |
| dc.subject | Formal verification | pt_BR |
| dc.subject | Correct software | pt_BR |
| dc.subject | UTF-8 | pt_BR |
| dc.subject.cnpq | CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO | pt_BR |
| dc.title | Verificação formal de uma implementação eficiente de UTF-8 | pt_BR |
| dc.type | Trabalho de conclusão de graduação | pt_BR |