Escribir correctamente algoritmos concurrentes es difícil. Las técnicas de comprobación habituales no ayudan mucho en el contexto de los programas concurrentes, debido a los comportamientos no deterministas de estos programas y al hecho de que algunos errores solo se manifiestan en un entorno específico (por ejemplo, en el modelo de memoria relajado de un hardware concreto).

La comprobación de modelos es una técnica de verificación formal que ayuda a descubrir fallos en los programas concurrentes mediante la exploración sistemática de varias trazas de ejecución de un programa en un entorno controlado.

En este proyecto, estamos desarrollando nuevas técnicas para abordar este problema, intentando mejorar las herramientas de comprobación de modelos existentes para programas concurrentes, y probándolas en proyectos de software del mundo real.