É difícil escrever corretamente algoritmos de execução simultânea. As técnicas comuns de teste não ajudam muito no contexto dos programas simultâneos, devido ao comportamento não determinístico desses programas e ao fato de que alguns bugs só podem se manifestar em ambientes específicos (por exemplo, no modelo de memória relaxada de determinado hardware).

A verificação de modelos é uma técnica formal de verificação que ajuda a revelar bugs em programas simultâneos explorando sistematicamente vários traços de execução de um programa em um ambiente controlado.

Neste projeto, estamos desenvolvendo técnicas inovadoras para abordar este problema, tentando melhorar as ferramentas existentes de verificação de modelos para programas simultâneos e testando essas ferramentas em campo, em projetos de software do mundo real.