Fazem parte dos métodos formais, técnicas e linguagens baseadas em modelos matemáticos que permitem a modelagem e especificação de sistemas de forma rigorosa em que sistemas de prova e algoritmos podem ser aplicados para verificar a consistência de especificações e correção de especificações e modelos. Pesquisas nesta área giram em torno, entre outras frentes, da busca por soluções que expandam o uso destes métodos na indústria de software. Mais especificamente, soluções para aumentar a eficiência dos algoritmos de verificação, soluções para contornar o problema da explosão de espaços de estados dos verificadores de modelos, técnicas e linguagens para especificação formal de sistemas na presença de informações incompletas, algoritmos para transformação e reparo de modelos estão entre os temas de pesquisa atuais.
Pesquisadores: Adolfo Duran, Aline Maria Santos Andrade