text: BLAST — статический анализатор Си-программ CADP (Construction and Analysis of Distributed Processes) — инструмент проектирования протоколов и распределенных систем CHESS — инструмент для тестирования многопоточных программ для .Net (управляемых) и Win32, 64 ISP — верификатор кода MPI-программ Java Pathfinder — свободный инструмент для проверки многопоточных Java-программ MoonWalker — свободный инструмент для проверки .Net-программ MRMC (Markov Reward Model Checker) NuSMV — символьный верификатор PRISM — вероятностный символьный верификатор Rabbit — верификатор для систем реального времени SPIN — верификатор общего назначения для проверки корректности распределенных программ и протоколов Vereofy — верификатор программ компонентных систем μCRL2 — свободный инструмент, основан на ACP UPPAAL — инструментарий для моделирования, верификации и валидации систем реального времени моделируемых как сети временных автоматов Zing — инструментарий от Microsoft для проверки модели состояний параллельного программного обеспечения, передающих сообщений программ и протоколов.