Métodos formais algébricos para verificação de programas

Resumo

Esta proposta visa, primordialmente, investigar a redução de problemas de análise estática de programas (i.e. geração de invariantes, análise automatizada de terminação de programas, etc) para problemas de Álgebra Linear. Na linha de novos métodos estáticos para análise estática de sistemas complexos, nossas investigações se voltarão para o desenvolvimento de algoritmos associados eficazes. Pretendemos fundamentar técnicas inéditas e eficientes que venham a formar o núcleo de novos algoritmos para automação de processos dedutivos, e de novos algoritmos para verificação de modelos complexos, para verificação de propriedades de segurança e de propriedades de vivacidade (i.e. terminação).Poderemos desenvolver métodos computacionais capazes de automatizar a descoberta de relações entre as variáveis de um programa, o qual pode conter laços, chamadas de sistemas e de funções. A generalização dos resultados teóricos hoje em uso em técnicas de prova automática de terminação, e o desenvolvimento de métodos computacionais eficazes para análise estática de terminação de programas, determinam um dos desafios e objetivos principais do nosso projeto. (AU)