Конференция завершена. Ждем вас на Saint HighLoad++ в следующий раз!

TLA+/TLC: формальный метод верификации конкурентных алгоритмов для инженеров Бэкенд, теория программирования

Доклад принят в программу конференции
Алексей Найденов
ITooLabs

CEO, а затем CSA собственной компании ITooLabs.
Проектирует, кодирует, преподает, управляет.

alexey.naidyonov@itoolabs.com
Тезисы

Разрабатывать конкурентные системы сложно. Самые плохие ошибки закрадываются в алгоритм еще на стадии проектирования, не находятся никакими тестами и ждут реальной нагрузки и своей уникальной последовательности событий, чтобы взорваться и всё испортить.

Находить такие ошибки можно, даже не написав ни строчки кода — если пользоваться методами формальной верификации алгоритмов. Таких методов много, но один из них — разработанный в 1999 г. Лесли Лампортом (Leslie Lamport) формализм TLA+ и инструмент верификации TLC — оказался ближе всего инженерам и приобретает все большую популярность.

Мы поговорим про TLA+/TLC, про PlusCal — транслируемый в TLA+ язык спецификации алгоритмов специально для инженеров, про инструментарий, а также про практики применения TLA+/TLC в реальных проектах.

Другие доклады секции Бэкенд, теория программирования