Local: Sala Multiuso CIC
Horário: 14h
Palestrante: Daniel Saad Nogueira Nunes (doutorando)
Título: A Grammar Compression Algorithm based on Induced Suffix Sorting
Resumo:We introduce GCIS, a grammar compression algorithm based on the induced suffix sorting algorithm SAIS, presented by Nong et al. in 2009. Our solution builds on the factorization performed by SAIS during suffix sorting. We construct a context-free grammar on the input string which can be further reduced into a shorter string by substituting each substring by its correspondent factor. The resulting grammar is encoded by exploring some redundancies, such as common prefixes between suffix rules, which are sorted according to SAIS framework. When compared to well-known compression tools such as Re-Pair and 7-zip under repetitive sequences, our algorithm is faster at compressing, presents a close compression ratio to Re-Pair, at the cost of being the slowest at decompressing.
Horário: 14h30
Palestrante: Washington Luis Ribeiro de Carvalho (doutorando)
Título: Nominal Matching Modulo A, C and AC
Resumo:A Nominal unification is first order unification with binders. Inside the class of first order equational problems, the case where no substitution is applied on the right-hand side (resp. both sides) of equationsis denominated matching (resp. equational checking).Efficient algorithms for equational checking, matching and unification within the nominal approach were already developed. Nominal unification and nominal matching are both quadraticaly bounded, whereas equational checking is log-linearly bounded. In addition, reasoning modulo equational theories is a very basic and recurrent issue in algebraic and logic systems. For instance, appending lists and evaluating a sequence of disjuctions are, respectively, associative (A) and associative-commutative (AC) operations. For this reason, standard fist order unification and matching modulo A, C and AC where extensively investigated since the late 1970s. We have explored equivalence checking within the nominal approach, on signatures with A, C and AC function symbols, and nominal unification with C function symbols. Now, we are presenting a (work in progress) formalisation (in Coq) of a nominal matching algorithm with A, C and AC function symbols.
Horário: 15h
Palestrante: Ariane Alves Almeida (doutoranda)
Título: Formalizando equivalência entre critérios de terminação em PVS
Resumo:A formalização de provas de equivalência entre critérios para análise de terminação para programas em uma linguagem funcional que modela a linguagem de especificação do assistente de prova PVS, chamada PVS0, será abordada nessa apresentação. Serão apresentados também detalhes da especificação da técnica de Pares Dependentes, que foi inicialmente desenvolvida para sistemas de reescrita, sendo necessária a sua adaptação para ser utilizada sobre os programas PVS0. Peculiaridades dessa formalização são o uso dos contextos de chamados utilizados para a definição da técnica de Grafos de Contextos de Chamados como parte dos pares dependentes. Além disso, discutiremos as dificuldades envolvidas em especificar funções que, embora seja totais, possuem uma especificação não trivial, como a função McCarthy 91.
Horário: 15h30
Palestrante: Paulo José de Souza Júnior (doutorando)
Título: Técnicas de Pré-configuração de Proteção para Redes Ópticas
Resumo:Com o surgimento das redes EON, as técnicas de proteção utilizadas para redes WDM são reavaliadas e a pesquisa de novas técnicas ganha importância. Este trabalho tem como objetivo comparar os principais métodos de pré-configuração de proteção com base na disponibilidade. A disponibilidade tem sido a principal métrica na implementação dos acordos de nível de contrato, e as técnicas de proteção são fundamentais para sua eficiência. As técnicas de pré-provisionamento e p-cycle são destacadas.
Profa Célia Ghedini Ralha (Este endereço de email está sendo protegido de spambots. Você precisa do JavaScript ativado para vê-lo.)
Coordenadora dos Seminários de Pós-Graduação em Informática 2018-1