Projetos de Doutorado, Mestrado e/ou IC Oferecidos

Verificação formal da correção de sistemas software/hardware críticos :

• Projetos de doutorado e mestrado com subprojetos de IC. Trabalha-se em cooperação com membros do Grupo de Métodos Formais do NIA/NASA LaRC, pesquisador César Muñoz.
• Descrição: Dois contextos de aplicação do assitente de prova PVS Specification and Verification System são explorados: 1. verificação da correção de sistemas de hardware e software e 2. da correção de algoritmos e protocolos criptográficos. Um dos objetivos, já no nivel de doutorado, é a definição e implementação de novas estratêgias de prova no sistema PVS, que permitam realizar demonstrações na teoria de reescrita e em teorias algébricas ainda não abrangidas pelo sistema PVS. Adicionalmente, 3. explora-se a aplicabilidade deste sistema de prova na verificação de protocolos criptográficos em cooperaçáo com o Prof. Anderson C. A. Nascimento do Departamento de Engenharia Elétrica da UnB.
• Alunos: quarto semestre de graduação em Matemática ou Computação, Mestrado em Matemática ou Informática ou Doutorado em Matemática. Alunos já envolvidos: Valnei Alves Fernandes (Mestre MAT/UnB 2004), André Galdino (Doutor em Matemática/UnB 2008), Rodrigo Borges Nogueira (Mestre em Informática/UnB 2008), Daniele Nantes (Mestre 2009 e Doutoranda em Matemática).
• Orientador: Prof. Mauricio Ayala Rincón.

• Joint project with Prof. Reiner W. Hartenstein leader of the Computer Structures Group of the Universität kaiserslautern (Germany) with "subprojetos de mestrado, finais e de IC". Funded by the CAPES/DFG Brazilian/German programme (2002/2004), CNPq/DFG (2008/2010).
• Descrição: After the occurrence of the seminal paper of Knuth and Bendix where rewriting was showed useful for the completation of algebraic theories as groups and monoids, the importance and applicability of Term Rewriting Theory and Systems have been made evident in a great variety of fields of Computer Science. Since then a lot of work has been done, that explore the simplicity of the computational formal framework given by rewriting for its application in areas such as automated theorem proving, program synthesis and verification, cryptography and code theory, combination of (the logical and functional) programming paradigms, development and implementation of higher order programming languages and proof assistants, etc. At some recent conferences some works propose the use of Term Rewriting Systems (TRS) for hardware design. E. g. Arvind from MIT has proposed a novel hardware design flow based on a Term Rewriting System, that will facilitate architectural exploration and dramatically reduce digital hardware design time. His goal is to raise the level of abstractions and to make greater use of automated synthesis Instead of digital system design, the TRS-based subject of our intended work is the development of a methodology for retargettable VLSI module generators for automatic generation of VLSI layout modules from expressions of an extended (Structural) Arithmetic / Logic expression Language (SALL). In contrast to Arvind's proposal our approach intends to make use of full custom structured VLSI design style, preferably based on wiring by abutment.
• Alunos: sexto semestre de graduação, projeto final em computação, Mestrado e Doutorado em Matemática ou Ciência da Computação. Alunos já envolvidos: Rinaldi Maia Neto (Mestrado CIC/UnB 2002), Rodrigo Borges Nogueira (PIBIC Eng. Mecatrônica/UnB 2003), Felipe Paulino Tavares (PIBIC Eng. Elétrica/UnB 2003), Thomas Mailleux Sant'Anna (Mestrado em Informática/UnB 2005), André Galdino (Doutor em Matemática/UnB 2008), Andréia Borges Avelar (Mestre 2009 e Doutoranda em Matemática/UnB), Carlos Morra (Dr. eng./KarlsruherIT 2010).
• Orientadores: Prof. Mauricio Ayala Rincón, Prof. Ricardo Jacobi e Prof. Carlos Llanos. Time alemáo: Prof. Reiner Hartenstein (Universität Kaiserslautern), Prof. Jürgen Becker e Carlos Morra.

• Projetos de doutorado e mestrado com subprojetos de IC. Neste tópico, trabalha-se em cooperação com a Prof. Fairouz Kamareddine, lider do grupo ULTRA (Useful Logics, Types, Rewriting and their Automation) da Heriot-Watt University, Edimburgo, Escócia.
• Descrição: substituição explícita é o mecanismo mais adequado para o tratamento formal preciso de implementações concretas tanto de linguagens de programação como de sistemas dedutivos. Sendo a operação de substituição essencial em processos computacionais elementares, como p. ex. a busca de redices em aplicações baseadas em técnicas dedutivas via reescrita e na implementações da unificação para o princípio de resolução das linguagens de programação lógica, se faz importante desenvolver um mecanismo formal preciso para a análise desta operação. A substituição explícita foi formulada originalmente no contexto do $\lambda\sigma$-calculus, variação do $\lambda$-calculus, como um mecanismo adequado para a análise destes processos sem os problemas típicos de colissão entre variáveis, geralmente resolvidos por renomeamento informal das variáveis envolvidas. Os problemas da informalidade da substituição são resolvidos pelo uso do $\lambda$-calculus na notação de de Bruijn, que troca nomes de variáveis por indices numéricos, e a substituição explícita. É de nosso interesse o estudo das propriedades dos calculi de substituição explícita e suas aplicações para a unificação de ordem superior. Para um subprojeto IC veja Visualization of the computational behaviour of the lambda calculus.
• Alunos: quarto semestre de graduação em Computação ou Matemática. Mestrado em Matemática ou Ciência da Computação. Alunos já envolvidos: Marcos de Andrade Gomes (PIBIC/CNPq 2002), Flávio L. C. de Moura (Mestre MAT/UnB 2002, aluno de Doutorado MAT/UnB, Bolsista CAPES).
• Orientador: Prof. Mauricio Ayala Rincón, Fairouz Kamareddine.
• Referências:
• M. Abadi, L. Cardelli, P.-L. Curien and J.-J. Levy, Explicit Substitutions, Journal of Functional Programming, 1(4):375-416, 1991.
• M. Ayala-Rincón and F. Kamareddine, On Applying the lambda s_e-Style of Unification for Simply-Typed Higher Order Unification in the Pure lambda Calculus. Special Issue of WoLLIC 2001 selected papers, John T. Baldwin, Ruy J. G. B. de Queiroz and Edward H. Haeusler, Eds. Matemática Contemporânea, Vol. 24:1-22, 2003.
• M. Ayala-Rincón, and F. Kamareddine, Unification via the Lambda s_e-Style of Explicit Substitutions, in the Logic Journal of the Interest Group on Pure and Applied Logics (IGPL), 9(4):489-523, Oxford University Press, 2001.
• M. Ayala-Rincón, and C. Muñoz, Explicit Substitutions and All That, postscript version. To appear in Colombian Journal of Computation, 1(1):47-71, 2000.
• G. Dowek, T. Hardin and C. Kirchner, Higher Order Unification via Explicit Substitution , Rapport de Recherche N 2709, INRIA, 1995. Available in G. Dowek home page.
• F.L.C. de Moura, F. Kamareddine and M. Ayala-Rincón, Second-Order Matching via Explicit Substitutions, (postscript, PDF). Proc. 11^th Int. Conf. on Logic Programming Artificial Intelligence and Reasoning LPAR 2004, F. Baader and A. Voronkov, Eds., Springer-Verlag, LNCS 3452, pp 433-448, March 2005.
• W. Snyder and J. Gallier, Higher Order Unification Revisited: Complete Sets of Transformations, Journal of Symbolic Computation, 8(1/2):101-140, 1989.

• Projeto de mestrado com subprojetos de IC.
• Descrição: Os indices de de Bruijn omitem o uso desnecessário de nomes de variáveis no lambda calculus. Desta maneira, problemas típicos da notação clássica do lambda calculus são evitados. O principal objetivo é estudar as propriedades da notação de de Bruijn e desenvolver uma estrutura de dados apropriada para a implementação natural das operações elementares do lambda calculus como são a beta redução e a eta redução.
• Alunos: segundo semestre de graduação em Computação ou Matemática. Mestrado em Matemática ou Ciência da Computação. Alunos já envolvidos: Flávio L. C. de Moura (Mestre MAT/UnB 2002, aluno de Doutorado MAT/UnB, Bolsista CAPES), Marrise Neves da Rocha (Bolsista PIBIC/CNPq MAT/UnB 2004), Aline Cosme da Cunha (Bolsista PIBIC/CNPq MAT/UnB 2005), Hélio Carneiro Ferreira (mestre MAT/UnB 2005, Bolsista DTI CNPq), Daniel Lima Ventura (mestrando MAT/UnB, Bolsista CNPq).
• Orientador: Prof. Mauricio Ayala Rincón.
• Referências:
• M. Abadi, L. Cardelli, P.-L. Curien and J.-J. Levy, Explicit Substitutions, Journal of Functional Programming, 1(4):375-416, 1991.
• M. Ayala-Rincón, F.L.C. de Moura and F. Kamareddine, Comparing Calculi of Explicit Substitutions with Eta-Reduction, (Postscript, 350 KB). In Pre-Proc. 9^th Workshop on Logic, Language, Information and Computation - WoLLIC 2002, pages 77-76, Rio de Janeiro, Brasil, July 30 - August 2, 2002. In Vol. 67 of the Elsevier ENTCS.
• M. Ayala-Rincón, F.L.C. de Moura and F. Kamareddine, Comparing and Implementing Calculi of Explicit Substitutions with Eta-Reduction, (Postscript, 277 KB). Annals of Pure and Applied Logic - WoLLIC 2002 selected papers, Ruy de Queiroz, Bruno Poizat and Sergei Artemov, Eds., Vol 134(1):5-41, 2005.
• R. Bird and R. Patersson, de Bruijn Notation as a Nested Datatype, Journal of Funtional Programming, 9(1):77-91, 1999.
• N. G. de Bruijn, Lambda Calculus Notation with Nameless Dummies , Indagationes Mathematicae, 34:381-392, 1972.
• R. Bird and O. de Moor, Algebra of Programming. C.A.R. Hoare Series Editor, 100th Title, Prentice Hall International Series in Computer Science, 1997.
• F.L.C. de Moura, M. Ayala-Rincón and F. Kamareddine, SUBSEXPL: a Tool for Simulating and Comparing Explicit Substitutions Calculi. 5^th International Workshop on the Implementation of Logics held in conjunction with the Proc. 11^th Int. Conf. on Logic Programming Artificial Intelligence and Reasoning LPAR 2004, (Tutorial postscript version, PDF) March 2005.

• Projeto de mestrado com subprojetos de IC.
• Descrição: Deseja-se estudar estruturas de dados e soluções "algorítmicas" (computacionais) adequadas para o problema de reconhecimento aproximado de padrões em palavras e ilustrar sua aplicabilidade no contexto de problemas reais na biologia computacional. O ponto de partida para tal estudo serão as árvores de sufixos [1,2,3,4,10] e os autômatos de sufixos [5], que têm sido demonstrados de grande aplicabilidade e eficiência para o tratamento básico destes problemas. Em particular, as árvores de sufixos são a estrutura de dados mais adequada para organizar a estrutura combinatória de palavras, permitindo assim resolver problemas como busca de repetições, reconhecimento de padrões, etc. de maneira ótima. Por outro lado os autômatos de sufixos foram demonstrados adequados para o tratamento eficiente do problema de reconhecimento aproximado de palavras [6,7], que é de grande aplicabilidade em biologia computacional. Assim, deseja-se especificamente analisar e verificar na prática a adequabilidade computacional do método proposto em [7] ou possíveis modificações deste para o tratamento de problemas reais de reconhecimento aproximado de padrões em biologia computacional. Parte importante do trabalho será verificar e comparar possibilidades de soluções propostas na literatura mais recentemente o que inclui novas estruturas de dados como os arranjos de sufixos e soluções sobre hardware não convencional [8,9,11,12].
• Alunos: quinto semestre de graduação em Computação ou Matemática. Mestrado em Matemática ou Ciência da Computação. Alunos já envolvidos:Camilo Bessoni (PIBIC/CNPq/UnB, MAT 2005), Claudio Celso Soares Oliveira (PIBIC/CNPq/UnB, CIC), Rodrigo Miranda (Mestrado em Informática/UnB) e Leon Solon (Mestrado em Informática/UnB, Bolsista CAPES 2005).
• Orientador: Prof. Maria Emilia Telles Walter e Prof. Mauricio Ayala Rincón.
• Referências:
• [1] P. Weiner, Linerar Pattern Matching Algorithms, IEEE 14th Annual Symposium on Switching and Automata Theory, pp 1-11, 1973
• [2] E.M. McCreight, A Space-Economical Suffix Tree Construction Algorithm. JACM, 23(2):262-272,1976
• [3] E. Ukkonen, On-Line Construction of Suffix-Trees. Algorithmica, 14:249-260, 1995
• [4] R. Griegerich and S. Kurtz. From Ukkonen to McCreight and Weiner: A Unifying View of Linear-Time Suffix Tree Construction. Algorithmica, 19:331-353,1997
• [5] M. Crochemore, Transducer and Repetitions. TCS, 45:63-86, 1986
• [6] G. M. Landau and U. Vishkin, Fast Parallel and Serial Approximate String Matching. J. of Algorithms, 10:157-169, 1989
• [7] P. Jokinen and E. Ukkonen, Two Algorithms for Approximating String Matching in Static Texts. LNCS 520, Proc. Mathematical Foundations of Computer Science, 1991
• [8] G. Navarro, Improved Approximate Patern Matching on Hypertext. TCS 237:455-463, 2000
• [9] R. Baeza-Yates and C. H. Perleberg, Fast and Practical Approximate String Matching, ...
• [10] M. Ayala-Rincón and P. D. Conejo, A Linear Time Lower Bound on McCreight and General Updating Algorithms for Suffix Trees, in Algorithmica, 37(3):233-241, Springer-Verlag, (Communicated by F. P. Preparata), 2003.
• [11] A. Boukerche, A.C.M.A. de Melo, M. Ayala-Rincón, T. M. Sant'ana, Parallel Smith-Waterman Algorithm for Local DNA Comparison in a Cluster of Workstations. Proc. 4^th Experimental and Efficient Algorithms - WEA 2005, Springer-Verlag, LNCS 3503, pp 464-475, 2005.
• [12] R. de C. Miranda and M. Ayala-Rincón, A Modification of the Landau-Vishkin Algorithm Computing Longest Common Extensions via Suffix Arrays, (pdf).
  • Complete version, in in Proc. XXXI CLEI, pp 41-50, 2005 (Talk).
  • Four page - extended abstract -, in Proc. Advances in Bioinformatics and Computational Biology BSB 2005, Springer-Verlag LNCS (LNBI) 3594:210-213, 2005.

---

Estudo de Árvores de Sufixos e Estruturas de Dados Alternativas para Representação Dinâmica de Texto :

• Projeto de mestrado com subprojetos de IC.
• Descrição: As árvores de sufixos são a estrutura de dados mais adequada para representação organizada da estrutura combinatória de palavras sobre um alfabeto finito. As propriedades desta estrutura de dados permitem soluções eficientes (e em certos casos ótimas) de importantes problemas computacionais como p.ex. reconhecimento de padrões em palavras, compressão de texto, etc. Lastimosamente, tem-se demonstrado que o mantinmento dinâmico de tal estrutura não é adequado para problemas onde as palavras ou textos mudam durante o processamento: dada a árvore de sufixos de um texto o custo de atualizar a árvore de sufixos após uma mudança do texto é praticamente o mesmo que o de constroir a árvore partindo do texto já modificado. É então importante analisar estruturas de dados alternativas, que junto com as árvores de sufixos permitam o aproveitamento destas no tratamento de problemas combinatórios em palavras que mudam dinâmicamente.
• Alunos: terceiro semestre de graduação em Computação ou Matemática. Mestrado em Matemática ou Ciência da Computação.
• Orientador: Prof. Mauricio Ayala Rincón.
• Referências:
• M. Ayala-Rincón and P. D. Conejo, A Linear Time Lower Bound on McCreight and General Updating Algorithms for Suffix Trees, in Algorithmica, 37(3):233-241, Springer-Verlag, (Communicated by F. P. Preparata), 2003.
• D. Gusfield, Algorithms on Strings, Trees and Sequences: Computer Science and Computational Biology. Cambridge University Press, 1997.
• G. Kucherov, M. Rusinowitch, Matching a set of strings with variable length don't cares, in Theoretical Computer Science 178:129-154, 1997.
• E. Ukkonen, On-line construction of suffix-trees, in Algorithmica 14:249-260, 1995.

• Projeto em andamento onde são bemvindos alunos interessados em subprojetos IC e de Mestrado.
• Descrição: O objetivo principal deste projeto é ilustrar graficamente via implementaçáo de applets Java os teoremas de equivalência clássicos entre modelos de computação e gramáticas e linguagens computacionais.
• Alunos: terceiro semestre de graduação em Computação ou matemática.
• Orientador: Prof. Haydée Werneck Poubel e/ou Prof. Mauricio Ayala Rincón. Alunos já envolvidos: Alison Hugo Rodrigues Silva (PIBIC/UnB, CNPq), Alexsandro Fernandes da Fonseca (Mestre CIC/UnB, CAPES) e Rodrigo Borges Nogueira (PIBIC/CNPq).
• Referências:
• M. Ayala-Rincón, A.F. da Fonseca, H.W. Poubel and J. de Siqueira, A Framework to Visualize Equivalences Between Computational Models of Regular Languages, Information Processing Letters, 84(1):5-16, Elsevier 2002.
• R. G. Taylor, Models of Computation and Formal Languages, Oxford University Press, 1998. Link to related software Deus Ex Machina from N. Savoiu. See license agreement and instructions in previous link when downloading local copy of this software (3 MB).
• A. H. R. da Silva, M. Ayala-Rincón, Simple applet for String Pattern Matching SAGAReP containing Knuth-Morris-Pratt, Boyer-Moore and Suffix-Tree pattern matching methods, Melhor projeto PIBIC-UnB/CNPq da área, 1999.
• A. H. R. da Silva, A.F. da Fonseca, M. Ayala-Rincón, Sistema de Animação Gráfica de Teoremas de Equivalência entre Modelos e Linguagens Computacionais - SAGEMoLiC, Simulação e visualização de teoremas de equivalência para o caso dos modelos e representações gramaticais das linguagens regulares, 2001.
• A.F. da Fonseca, A.H.R. da Silva, M. Ayala-Rincón, H.W. Poubel and J. de Siqueira, Animation of Relations between Computational Models and Their Language Representations, (Gziped Postscript, 64 KB). In Bulletin of The European Association for Theoretical Computer Science - EATCS, 74:235-241, June 2001.

Utilização de Técnicas Categóricas na Teoria da Reescrita :

• Projetos de mestrado com subprojetos de IC.
• Descrição: Propõe-se o estudo sistemático da teoria de categorias computacional aplicada à solução de problemas da teoria de reescrita. Em particular deseja-se compreender aplicações recentes da teoria de categorias na demonstração de resultados clássicos da área de sistemas de reescrita de termos. Serão estudados o teorema de preservação da propriedade de confluência de Toyama, para união disjunta de sistemas de reescrita confluentes, e as condições necessárias para garantir a modularidade da propriedade de terminação.
• Alunos: quarto semestre de graduação em Matemática ou Mestrado em Matemática. Alunos já envolvidos: Wellington Barros e Barbosa (Mestre MAT/UnB, CAPES) e Helio Carneiro Ferreira (PIBIC/CNPq/UnB).
• Orientador: Prof. Haydée Werneck Poubel ou Prof. Mauricio Ayala Rincón.
• Referências:
• Segunda parte das Notas de Aula da disciplina de Introdução à Computação: M. Ayala-Rincón, Fundamentos da Programação Lógica e Funcional - O Princípio de Resolução e a Teoria de Reescrita -, Lecture Notes, Department of Mathematics, University of Brasilia, third version, December 1998. In Portuguese. Postscript Chapter by Chapter available in http://www.mat.unb.br/~ayala/academics.html.
• F. Baader and T. Nipkow , Term Rewriting and All That . Cambridge University Press, 1998.
• R. F. C. Walters, Categories and Computer Science. Cambridge Computer Science Texts, 1991.
• R. Bird and O. de Moor, Algebra of Programming. C.A.R. Hoare Series Editor, 100th Title, Prentice Hall International Series in Computer Science, 1997.
• E. Moggi and G. Rosolini (Eds), Category Theory and Computer Science, Seventh Int. Conference, CTCS'97, Santa Margherita Ligure, Italy, September 1997. Lecture Notes in Computer Science 1290. Springer, 1997.

• alunos interessados em projetos de Iniciação Científica na área, devem ter em conta as datas de aplicação para bolsas IC do programa PIBIC/CNPq/UnB. Geralmente o prazo inscrição no PIBIC é no mês de maio; assim, que se recomenda entrar em contato com os orientadores no mês de abril de cada ano.
• Alunos do Mestrado em Matemática interessados em desenvolver sua dissertação na área, devem entrar em contato com os orientadores preferivelmente antes do inicio do terceiro semestre indicando seu interesse. As disciplinas básicas recomendadas para estes alunos são Introdução à Computação e Lógica Formal.
• Alunos interessados em ingressar no programa de Doutorado em Matemática, na área de Semântica e Lógica da Computação, devem entrar em contato com o Prof. Mauricio Ayala Rincón. Orientação neste nível está viavilizada a partir do primeiro semestre de 2002. Normas do programa de doutorado no MAT/UnB e do ingresso na página do MAT/UnB.
• Alunos interessados em ingressar no programa de Mestrado em Informática e desenvolver sua dissertação em projetos da área, devem entrar em contato com o possivel orientador para formular um projeto segundo os prazos e normas para o ingresso no Programa de Mestrado em Informática da UnB.