O grupo de pesquisa Theoretical Computer Sciencetem desenvolvido e utilizado técnicas para garantir o desenvolvimento de software correto e eficiente, contribuindo com a área de engenharia de software e outras.Uma questão fundamental no desenvolvimento de um software é garantir que este é realmente uma solução para o problema proposto. Para realizar tal tarefa, deve-se primeiro construir um modelo da solução (especificação) utilizando uma linguagem formal. Tendo este modelo formal como base, pode-se:- realizar provas matemáticas que garantem que este modelo possui as propriedades requisitadas (verificação).;- analisar se a solução proposta é aceitável do ponto de vista dedesempenho, indicando quais as melhores estratégias para implementação a serem seguidas;- validar o modelo através de simulações;- realizar o desenvolvimento do software podendo-se provar que aimplementação está correta (geração de código correto).
