Otro título
Formalization of ACCE technique on Coq formal proof management system
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.
Institución
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.
