Topics of Research:

Group Members:


Graduate Students and Researchers:

Undergraduate Students:

Former Members:

Former Graduate Students:

Former Undergraduate Students:


  • A PVS theory for abstract rewriting systems trs.
  • ELAN specification of processors over the AX RISC architecture. Tared file containing the prototype. For a description see the paper Applying ELAN Strategies in Simulating Processors over Simple Architectures, (Postscript, 274 KB).
  • ELAN specification of reconfigurable systems for algebraic operations. Tared file containing the prototypes. For a description see the paper Efficient Computation of Algebraic Operations over Dynamically Reconfigurable Systems Specified by Rewriting-Logic Environments, (PDF).
  • SUBSEXPL: an OCAML implementation of reduction via the explicit substitution calculi: lambda sigma, lambda se, the suspension calculus and a refinement of the suspension calculus which combines steps of beta-contraction.
  • Java applet SAGAReP illustrating string pattern matching algorithms.
  • Java applet SAGEMoLiC illustrating equivalence theorems between Finite State and Pushdown Automata and their related classes of languages and gramars. And that allows for normalizations of Context Free Grammars (to their Greibach and Chomsky NFs)
  • Applet on approximate string pattern matching via suffix trees. A nice implementation of Ukkonen's suffix trees based method implemented by some our best undergraduate students as a project of Analysis on Algorithms during the Second semester 2001.
  • Applet for optimizing Finite State Automata developed by students for the course on Formal Languages and Automata during the first semester 1999


Academics (including offered courses for the second semestrer 2001)

Offered supervision on undergraduate and graduate projects


Computing Resources

Links & Other Services


Comments to webmasterTC n@Spam mat.unb.br

Feb 26, 1997