Banca de DEFESA: Thiago Mendonça Ferreira Ramos

Uma banca de DEFESA de DOUTORADO foi cadastrada pelo programa.
DISCENTE : Thiago Mendonça Ferreira Ramos
DATA : 12/07/2023
HORA: 15:00
LOCAL: Sala Múltiusos CIC com participação remota dos membros externos
TÍTULO:

Verifying the Computational Properties of a
First-Order Functional Mode

PALAVRAS-CHAVES:

Turing Completude, Problema da Parada, Teorema de Rice, Teorema do Ponto Fixo, Problema da Correspondencia de Post, Problema da Palavra, Indecidibilidade

PÁGINAS: 91
RESUMO:

Este trabalho descreve a mecanização de propriedades computacionais de um modelo funcional que tem sido aplicado para automatizar o raciocínio sobre a terminação de programas. A formalização foi desenvolvida no assistente de provas de lógica de ordem superior, chamado Prototype Verification System (PVS). O modelo de linguagem foi projetado para imitar o fragmento de primeira ordem de especificações funcionais e é chamado PVS0. Foram considerados dois modelos computacionais: o primeiro modelo especifica um programa funcional por meio de uma única função (modelo single-function PVS0, ou SF-PVS0), e o segundo modelo permite a especificação simultânea de múltiplas funções (modelo multiple-function} PVS0, ou MF-PVS0). A semântica operacional da recursão na especificação do modelo SF-PVS0 suporta a recursão sobre o programa completo.

Por outro lado, em programas MF-PVS0, as chamadas funcionais são permitidas para todas as funções especificadas no programa. Este trabalho tem como objetivo certificar matematicamente a robustez dos modelos PVS0 como modelos computacionais universais. Para isso, propriedades cruciais e teoremas foram formalizados, incluindo Turing Completude, a indecidibilidade do Problema da Parada, o teorema da recursão, o teorema de Rice e o teorema do Ponto Fixo. Além disso, o trabalho discute avanços na indecidibilidade do Problema da Palavra e do Problema da Correspondência de Post.

A indecidibilidade do Problema da Parada foi formalizada considerando a avaliação semântica de programas PVS0 que foram aplicados na verificação da terminação de especificações em PVS. A equivalência entre a avaliação funcional e predicativa de operadores foi fundamental para esse objetivo. Além disso, a composicionalidade de programas MF-PVS0, habilitada diretamente pela possibilidade de chamar diferentes funções, torna fácil a formalização da Turing Completude. Portanto, enriquecer o modelo foi uma decisão de design importante para simplificar a mecanização dessa propriedade e dos teoremas mencionados acima.

MEMBROS DA BANCA:
Externo à Instituição - NATARAJAN SHANKAR
Externo à Instituição - DOMINIQUE LARCHEY-WENDLING
Externa à Instituição - LAURA TITOLO
Presidente - 2180096 - MAURICIO AYALA RINCON
Interno - 1702036 - VANDER RAMOS ALVES