Formalização de ACCE no provador de teoremas Coq

Abstract

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.

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.