Sistemas computacionais são frequentemente utilizados em aplicações críticas como controladores de máquinas industriais aonde falhas podem ter consequências graves. Mesmo em aplicações não industriais erros são frequentemente inaceitáveis. Por exemplo, em um sistema de comércio eletrônico erros podem levar desde a perda de clientes por insatisfação com o serviço até a perda financeira, se transações comerciais não forem completadas corretamente. Contudo, devido ao paralelismo e às restrições temporais comumente presentes neste tipo de aplicações, torna-se extremamente complexo projetá-las corretamente. Técnicas tradicionais para se verificar se o sistema está correto como teste e simulação não garantem que o sistema está correto, pois não exploram todos os comportamentos e podem não detectar erros potencialmente graves. Um método alternativo que tem se mostrado viável é provar que um modelo do sistema analizado satisfaz ou não suas especificações utilizando métodos formais. Tradicionalmente considerados como de interesse teórico, estes métodos têm ganho aceitação em ambientes industriais devido ao desenvolvimento de algoritmos mais eficientes para a representação de modelos. Por exemplo, os primeiros algoritmos para verificação de modelos (model checking) eram capazes de representar modelos com no máximo 10E4 ou 10E5 estados. Na década de 90, algoritmos simbólicos foram desenvolvidos que utilizam diagramas de decisão binários (binary decision diagrams, BDDs) para representação interna do modelo. Estes algoritmos conseguem verificar propriedades de modelos com mais de 10E20 estados. Trabalhos recentes aumentaram a eficiência deste método e o aplicaram na verificação de aplicações críticas como sistemas de tempo-real em software e hardware. Contudo, verificação de modelos ainda é uma técnica de utilização difícil. Existe uma limitação no tamanho dos sistemas que podem ser verificados, uma vez que o tamanho da representação interna pode crescer exponencialmente durante a verificação. Este problema é conhecido como explosão de estados. Diversas técnicas podem ser usadas para diminuir os efeitos da explosão de estados, como por exemplo, raciocínio composicional ou algoritmos especiais de verificação. Este projeto se propõe a extensão destes trabalhos através do estudo de técnicas especiais de verificação que evitem a explosão de estados e permitam a utilização de métodos formais em problemas maiores do que os possíveis hoje em dia. Além disto, o projeto prevê a aplicação de métodos formais em novas áreas que possam se beneficiar desta ferramenta. Pretendemos inicialmente explorar a aplicação de verificação formal na área de comércio eletrônico.