Правильно писать алгоритмы параллельных вычислений очень сложно. Традиционные методики тестирования мало помогают в случае параллельно выполняемых программ — это связано с недетерминированным поведением таких программ и с тем, что некоторые ошибки появляются только в определенном окружении (например, в ослабленной модели памяти конкретного аппаратного обеспечения).

Проверка модели — методика формальной верификации, которая помогает найти ошибки в параллельно выполняемых программах, систематически изучая трассировку различных вариантов выполнения в управляемом окружении.

В рамках этого проекта мы разрабатываем инновационные методики для решения этой задачи, пытаясь улучшить существующие инструменты проверки моделей для параллельно выполняемых программ и протестировать их на реальных проектах разработки ПО.