TLA+/TLC: формальный метод верификации конкурентных алгоритмов для инженеров / Алексей Найденов