TLA+/TLC: практичный инструмент формальной верификаций алгоритмов. Алексей Найденов (ITooLabs).
Разрабатывать конкурентные системы сложно. Самые плохие ошибки закладываются в алгоритм, не находятся никакими тестами, и ждут своей уникальной последовательности событий, чтобы взорваться и всё испортить. Но находить такие ошибки можно, даже не написав ни строчки кода на Go -- если воспользоваться методами формальной верификации. Один из таких методов — разработанный Лесли Лампортом формализм TLA+ и инструмент верификации TLC -- идеально подходит верификации конкурентных систем на Go. Мы поговорим про TLA+/TLC, про PlusCal — транслируемый в TLA+ язык спецификации алгоритмов специально для инженеров, а также про практики применения TLA+/TLC в проектах на Go.
Видео TLA+/TLC: практичный инструмент формальной верификаций алгоритмов. Алексей Найденов (ITooLabs). канала GopherCon Russia
Видео TLA+/TLC: практичный инструмент формальной верификаций алгоритмов. Алексей Найденов (ITooLabs). канала GopherCon Russia
Показать
Комментарии отсутствуют
Информация о видео
Другие видео канала
Building an Autoscaling HTTP Proxy for Kubernetes. Aaron SchlesingerGeneric Programming in Go. Vladimir VivienGolang race detector. Neven Miculinic, Kraken Systems.Прозрачный gRPC-proxy один-ко-многим. Андрей СмирновA tour of xbar code. Mat RyerMessage-driven application made easy with Watermill. Robert Laszczak, Three Dots Labs.Javascript в Go: как мы храним интерпретируемую логику в конфиге. Алексей Шайхалеев, Aviasales.ruКак измерить настроение кода в Git репозитории. Вадим Марковцев, source{d}GopherCon Russia 2018. Как это былоGopherCon Russia 2019. Как это было.Встраивание в Go интерпретатора JS для реализации бизнес-логики. Алексей Найденов, ITooLabsGo's Hidden Pragmas. Dave CheneyПроблемы разработки базы данных числовых временных рядов с нуля на Go. Александр Вишератин, ИТМО.Воркшоп: TLA+/TLC: практичный инструмент формальной верификаций алгоритмов. Алексей НайденовChatting through Go. Joan López de la Franca Beltran, Atrápalo.Знакомство с гео-библиотекой s2 от Google и примеры ее использования в Badoo. Марко Кевац, Badoo.Go Profiling from Bottom Up. Felix GeisendörferОптимизация работы с PostgreSQL в Go: от 50 до 5000 RPS. Иван ОсадчийBitmap indexes. Marko Kevac, Badoo.Фаззинг: новое юнит тестирование. Дмитрий Вьюков, Google.