Banca de QUALIFICAÇÃO: WASHINGTON CAVALCANTE DA SILVA

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE : WASHINGTON CAVALCANTE DA SILVA
DATA : 27/11/2017
HORA: 09:30
LOCAL: Sala de seminários do DMAT
TÍTULO:

Especificação e Verificação de Protocolos de Votação em Lógica Linear com Focusing
Resumo

PALAVRAS-CHAVES:

Lógica linear, focusing, Sistemas de Transição, Protocolo de Votação

PÁGINAS: 80
RESUMO:

A lógica linear (LL) permite especificar sistemas computacionais de modo mais coerente do que as lógicas tradicionais, por considerar fórmulas como recursos que podem ser consumidos e/ou produzidos. Além disso, do ponto de vista da teoria da prova, a LL reconcilia o aspecto construtivo da lógica intuicionista com a simetria da clássica. Desta maneira, é possível, de uma forma mais flexível, modelar estados de um sistema como fórmulas lógicas, e as transições entre esses estados como etapas na construção de uma prova. No entanto, a busca de provas, em geral, não é determinística, pois existem diferentes maneiras de se provar a mesma proposição. Visando reduzir esse problema, um sistema de provas focado, conhecido como focusing, pode ser utilizado nesse processo de busca. Esse sistema focado, considerado uma forma normal para provas em LL, reduz a ocorrência de provas não essenciais que são sintaticamente diferentes, mas equivalentes no final do processo. Neste trabalho, é apresentada a prova da completude desse sistema, bem como de propriedades necessárias para a demonstração dessa prova. Além disso, o sistema focado será utilizado para especificação e verificação de protocolos de votação, que  definem como deve ser escolhido um candidato, feita uma contagem de votos, e divulgado o resultado de uma eleição. Para que isso seja possível, dois protocolos de votação serão especificados formalmente utilizando sistemas de transição, que modelam de forma natural os estados e comportamento de tais protocolos. Junto a isso, para cada sistema, um encoding em LL será definido e demonstrado que sua especificação é correta, ou seja, que um passo focado representa uma determinada transição no sistema de estados modelado. 
Além disso, propriedades inerentes aos protocolos de votação, como a garantia que o resultado da eleição reflete o desejo dos eleitores, serão apresentadas e demonstradas através de provas no sistema focado. 

MEMBROS DA BANCA:
Interno - 2114893 - CARLOS ALBERTO OLARTE VEGA
Interno - 1143603 - ELAINE GOUVEA PIMENTEL