Banca de DEFESA: VITORIA MARIA PENA MENDES

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE: VITORIA MARIA PENA MENDES
DATA : 30/04/2024
HORA: 08:00
LOCAL: Centro de Informática - Auditório
TÍTULO:

An Updated Theory for Communicating Sequential Processes in Coq

PALAVRAS-CHAVES:

Communicating Sequential Processes, CSP, Coq, Assistente de 
provas, Extensão para o VSCode

PÁGINAS: 87
RESUMO:

A habilidade de um sistema realizar operações simultâneas é conhecida como 
concorrência. Em sistemas concorrentes, o grande número de maneiras nas 
quais os componentes podem interagir entre si eleva significativamente a 
complexidade de analisar o comportamento desses sistemas. CSP 
(\emph{Communicating Sequential Processes}) introduz uma notação 
conveniente para descrever precisamente sistemas concorrentes. Ao longo dos 
anos, ferramentas computacionais foram desenvolvidas para permitir a 
análise de especificações em CSP, tais como: a ferramenta 
\emph{Failures-Divergence Refinement} (FDR) e teorias em Isabelle (por 
exemplo, CSP-Prover, HOL-CSP). Anteriormente, uma caracterização inicial de 
CSP foi desenvolvida em Coq: CSP${\text{Coq}}$. Aqui, estendeu-se 
significativamente as possibilidades de usar CSP para raciocinar sobre 
concorrência em Coq. Agora, há suporte para comunicações compostas, 
processos parametrizados e operadores de CSP que não foram considerados 
previamente. Condições de boa formação são também formalizadas em Coq e 
táticas de automação de prova são fornecidas. Além disso, foi desenvolvida 
uma extensão para o VSCode que converte automaticamente especificações em 
CSP${\text{M}}$ (o dialeto em ASCII de CSP) para CSP$_{\text{Coq}}$.

MEMBROS DA BANCA:
Interno - 2382523 - GUSTAVO HENRIQUE PORTO DE CARVALHO
Presidente - 1670543 - JULIANO MANABU IYODA
Externo à Instituição - SIDNEY DE CARVALHO NOGUEIRA - UFRPE