Saltar para o conteúdo principal

FCCNserviços digitais da FCT

Consulte informações sobre apoios e financiamentos científicos em Portugal

Atividade Financiada

VeriFixer: Reparação Automática para Linguagens de Programação com Suporte para Verificação

VeriFixer: Automated Repair for Verification-Aware Programming Languages

Referência
2023.15557.PEX
Data de Início do Projeto
2025-02-17
Data de Fim do Projeto
2027-02-16
Investigador Principal
Área Científica
Ciências exatas
Programa de Financiamento
Concurso de Projetos Exploratórios em Todos os Domínios Científicos 2023

Resumo

O software está cada vez mais presente no nosso dia a dia: desde o telemóvel que nos acompanha para todo o lado, até aos dispositivos médicos que diagnosticam e tratam os nossos problemas de saúde. É agora mais importante do que nunca garantir que o software não contém falhas. Além disso, com a crescente adoção de tecnologias digitais, a quantidade de dados digitais recolhidos e trocados por estas tecnologias atingiu níveis nunca antes vistos. É importante garantir que o software que suporta estas tecnologias não contém falhas, as quais podem resultar, por exemplo, no vazamento de informações sigilosas ou dados corrompidos/incompletos que levam a falhas dos sistemas. Falhas em software podem ter consequências catastróficas, como já foi comprovado muitas vezes no passado. No entanto, escrever software confiável, i.e, sem falhas, não é trivial. Reparação Automática de Programas (RAP), o processo de identificar automaticamente uma correção para uma determinada falha, é uma abordagem promissora para aumentar a qualidade do software, ajudando os programadores no processo de correção de seus programas. No entanto, em geral, o RAP é baseado em critérios de correção fracos, como um conjunto de testes, considerando-se que o programa está corrigido quando passa em todos os testes com sucesso. Tal fornece algumas garantias, mas não garante que o programa está correto. Como disse Edsger Dijkstra:  testes podem mostrar a presença de erros, mas nunca a sua ausência. Testar é suficiente em muitos contextos, mas, em sistemas críticos, são necessárias garantias adicionais que podem ser obtidas por meio da verificação de software, que garante matematicamente que o software se comporta exatamente como pretendido, em relação a uma determinada especificação ou propriedade formal. Várias linguagens e sistemas de programação com suporte para verificação, onde construções lógicas como pré e pós-condições, invariantes e asserções fornecem garantias sobre a correção do programa, estão disponíveis e permitem a verificação juntamente com o desenvolvimento do código. Ao usá-las para escrever código, falhas são geralmente indicadas por um verificador que avisa o utilizador sobre violações da sua especificação. No entanto, apesar da disponibilidade de especificações formais que podem atuar como critérios fortes de correção para RAP, os utilizadores têm de corrigir os seus programas manualmente, pois o trabalho existente em RAP para linguagens com suporte para verificação ainda é escasso. O principal objetivo deste projeto é desenvolver técnicas para a reparação automática de programas escritos numa linguagem de programação com suporte para verificação. Devido à natureza exploratória deste projeto, vamo-nos concentrar em programas Dafny (Leino, 2010), mas as técnicas serão aplicáveis ??a outras linguagens e sistemas com suporte para verificação, como VCC (Dahlweid et al., 2009), KeY ( Ahrendt, 2016) e Verus (Verus, 2022). A reparação será guiada pela especificação formal, ou seja, a especificação formal será considerada correta e um programa que não satisfizer a especificação será automaticamente reparado para satisfazê-la. A visão de curto prazo é construir uma ferramentas de código aberto que apoie os utilizadores na correção de falhas em linguagens de programação com suporte para verificação e fornecer à comunidade conjuntos de dados de referência com exemplos de código do mundo real para apoiar novos desenvolvimentos nesta área, e comos quais os resultados deste projeto serão avaliados. O objetivo geral é incentivar uma adoção mais ampla de linguagens de programação com suporte para verificação e reduzir o esforço de reparação de programas escritos nessas linguagens. Os resultados deste projeto resultarão de uma estreita colaboração entre investigadores do INESC TEC, INESC-ID Lisboa e Carnegie Mellon.

Instituições

Instituições Principais

  • Instituto de Engenharia de Sistemas e Computadores Tecnologia e Ciência (INESC TEC)

Outras Instituições

  • Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento em Lisboa (INESC-ID)
  • Computer Science Department, Carnegie Mellon University (CSD/CMU)

Financiamento 49.354,41 €

Fundação para a Ciência e a Tecnologia (FCT) - Portugal

49.354,41 €