Automated Program Repair of Arithmetic Programs in Dafny: Repairing Simple Arithmetic Programs EVALUATED

Detalhes: Escrever software é difícil. Seria incrível ser capaz de escrever programas sem bugs, ou pelo menos escrever software, e ter a possibilidade de encontrar os bugs sem perder horas em debugging. Para além de facilmente encontrar os bugs, receber sugestões de como os corrigir em tempo útil seria uma ferramenta excelente para propulsionar o desempenho de qualquer programador. Nesta tese documentamos o processo que utilizá-mos para criar uma framework para reparar programas de aritmética com bugs em Dafny. Para reparar programas, utilizámos um sintetizador já existente, assim como um verificador, para reparar programas Dafny com bugs. No processo, criámos uma framework extensível que permite adicionar integração com outros geradores. A solução proposta identifica expressões de código problemáticas recorrendo ao verificador da linguagem Dafny, cria os Expression Templates, traduz o estado actual do programa para a linguagem do sintetizador (caso a sua linguagem nativa não seja Dafny), e sugere uma correção para um bug que foi encontrado.

Discussão: novembro 22, 2022, 14:30

Publicação

Obra sujeita a Direitos de Autor

Orientação

AUTOR

Hugo Rafael Fecha Martins (ist190727)

ORIENTADOR

João Fernando Peixoto Ferreira

Departamento de Engenharia Informática (DEI)

Professor Auxiliar

ORIENTADOR

Alexandra Mendes

FEUP - Faculdade de Engenharia da Universidade do Porto

Assistant Professor