Repositório Digital

A- A A+

Formalização de ACCE no provador de teoremas Coq

.

Formalização de ACCE no provador de teoremas Coq

Mostrar registro completo

Estatísticas

Título Formalização de ACCE no provador de teoremas Coq
Outro título Formalization of ACCE technique on Coq formal proof management system
Autor Tanus, Felipe de Oliveira
Orientador Moreira, Alvaro Freitas
Data 2013
Nível Graduação
Instituição Universidade Federal do Rio Grande do Sul. Instituto de Informática. Curso de Ciência da Computação: Ênfase em Ciência da Computação: Bacharelado.
Assunto Lógica matemática
Teoria : Computação
[en] ACCE
[en] Coq
[en] Fault Tolerance
[en] LLVM
[en] VeLLVM
Resumo Este trabalho descreve uma implementação da transformação ACCE em Coq. A técnica visa permitir que um programa detecte e corrija automaticamente erros de controle de fluxo causados por soft errors. A transformação é aplicada na linguagem intermediária LLVM IR. Para isso, é utilizado o VeLLVM, que disponibiliza uma implementação de uma semântica formal para a linguagem LLVM IR. Esse é o primeiro passo para a construção de provas formais sobre a técnica ACCE.
Abstract This work describes an implementation in Coq of ACCE. This technique aims to allow a software to detect and automatically fix control flux errors, generaly caused by soft errors. This transformation is applied on the LLVM Intermediate language. To accomplish this, the LLVM IR formal semantic presented by the VeLLVM is used. This is the first step to write proofs about the ACCE technique.
Tipo Trabalho de conclusão de graduação
URI http://hdl.handle.net/10183/66076
Arquivos Descrição Formato
000870876.pdf (605.5Kb) Texto completo Adobe PDF Visualizar/abrir

Este item está licenciado na Creative Commons License

Este item aparece na(s) seguinte(s) coleção(ões)


Mostrar registro completo

Percorrer



  • O autor é titular dos direitos autorais dos documentos disponíveis neste repositório e é vedada, nos termos da lei, a comercialização de qualquer espécie sem sua autorização prévia.
    Projeto gráfico elaborado pelo Caixola - Clube de Criação Fabico/UFRGS Powered by DSpace software, Version 1.8.1.