Banca de QUALIFICAÇÃO: Nikson Bernardes Fernandes Ferreira

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE : Nikson Bernardes Fernandes Ferreira
DATA : 27/10/2022
HORA: 16:00
LOCAL: Sala Multiusos do CIC (participação híbrida do membro externo)
TÍTULO:

Melhorando a segurança de programas numéricos

PALAVRAS-CHAVES:

Análise de Programas, Aritmética de Ponto Flutuante, Detecção e Evasão, Métodos
Formais, PVS

PÁGINAS: 30
RESUMO:

Este trabalho discute como a precisão dos erros de arredondamento envolvidos em implementações
reais do sistema de gerenciamento da NASA para veículos não tripulados DAIDALUS afetam a segurança
geral do sistema. A biblioteca DAIDALUS fornece definições formais para os conceitos de Detecção
e Evasão em aviônica demonstrados mecanicamente no assistente de provas PVS. No entanto, tais
verificações são apenas certificados do bom comportamento da especificação do ponto de vista lógico, o
que não garante a precisão dos algoritmos implementados sob restrições aritméticas de ponto flutuante.
Nossa análise assume o padrão IEEE 754 de ponto flutuante, implementados em diversas linguagens de
programação, e a técnica de verificação se baseia na geração de uma especificação de primeira ordem dos
cálculos numéricos. Uma característica proeminente da abordagem é dividir a especificação em fatias
definidas de acordo com os diferentes ramos de computação. O fatiamento é crucial para simplificar a
análise formal das computações com aritmética de ponto flutuante.

MEMBROS DA BANCA:
Presidente - 2180096 - MAURICIO AYALA RINCON
Interno - 1702036 - VANDER RAMOS ALVES
Externa à Instituição - LAURA TITOLO