동시 알고리즘을 올바르게 작성하는 것은 어렵습니다.일반적인 테스트 기법은 이러한 프로그램의 비결정적 동작과 더불어 일부 버그가 특정 환경(예: 특정 하드웨어의 완화된 메모리 모델)에서만 나타날 수 있다는 사실 때문에 동시 프로그램의 맥락에서 그다지 도움이 되지 않습니다.

모델 검사는 제어된 환경에서 프로그램의 다양한 실행 추적을 체계적으로 탐색하여 동시 프로그램의 버그를 발견하는 데 도움을 주는 공식적인 검증 기법입니다.

동시 프로그램에 대한 기존 모델 검사 도구를 개선하고 실제 소프트웨어 프로젝트에서 현장 테스트를 수행하는 등 이 프로젝트에서는 이 문제를 해결하기 위해 새로운 기법을 개발하고 있습니다.