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:
Specification and verification of voting protocols using focused linear logic.

PALAVRAS-CHAVES:
linear logic, focusing, transition systems, voting procolos.

PÁGINAS: 80
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Matemática
RESUMO:
Linear logic (LL) allows us to specify computational systems more accurately than traditional logics. This is mainly due to the fact that formulas are seen as resources that can be consumed and produced during a proof. From the point of view of Proof Theory, LL reconciles the constructive aspect of intuitionistic logic with the symmetry of rules in classical logic. Hence, LL offers a more flexible way to model states of a system as well as transitions among those states. We note that the proof search procedure is inherently non-deterministic since there are different ways of proving the same proposition. In order to tame this problem, focused systems have been proposed aiming at reducing the number of choices during the proof search procedure. Roughly, a focused system considers  normal form proofs, thus eliminating the occurrences of nonessential proofs that are syntactically different but equivalent. In this work, we prove the completeness of a focused system for LL as well as some other essential properties of this system. In addition, we use the focused system for specifying and verifying voting protocols. Such systems define how a candidate is chosen by tallying votes and computing the final result of an election. We formally specify two voting protocols using transition systems, which naturally model the states and behavior of such protocols. For each system, an encoding in LL is defined and we show that our specification is correct: a focused step corresponds exactly to a transition in the modeled system. Finally, we verify important properties of the voting protocols such as the fact that the system ensures that the election result reflects the voters' desire.

MEMBROS DA BANCA:
Interno - 2114893 - CARLOS ALBERTO OLARTE VEGA
Interno - 1143603 - ELAINE GOUVEA PIMENTEL
Notícia cadastrada em: 13/11/2017 07:12
SIGAA | Superintendência de Tecnologia da Informação - (84) 3342 2210 | Copyright © 2006-2024 - UFRN - sigaa03-producao.info.ufrn.br.sigaa03-producao