Podlodka #268 – Формальные методы и верификация программ
Podlodka Podcast
Russian - May 17, 2022 08:23 - 1 hour - 213 MB - ★★★★★ - 39 ratingsTechnology Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Мечтаете, чтобы ваше ПО было сверх надежным, но грустите, ведь даже самый большой набор тестов не гарантирует 100% работоспособность кода на всех кейсах? На помощь придет верификация ПО с помощью формальных методов! Опишем спецификацию на программу с помощью математических языков и докажем какие-нибудь ее свойства. Не обещаем, что будет просто, но точно будет интересно! Вместе с профессором Национального Университета Сингапура Ильей Сергеем разобрали верификацию не только на простых задачах, но и в проектах с огромной кодовой базой и распределенными вычислениями. Обсудили истории успеха из реальных проектов, основные сложности этого подхода и направления активных исследований применения формальных методов в разработке ПО.
Оставляйте заявку и бесплатно переносите проекты на гибкую и мощную инфраструктуру Selectel: https://slc.tl/gzpzo
Поддержи лучший подкаст про IT:
www.patreon.com/podlodka
Также ждем вас, ваши лайки, репосты и комменты в мессенджерах и соцсетях!
Telegram-чат: https://t.me/podlodka
Telegram-канал: https://t.me/podlodkanews
Страница в Facebook: www.facebook.com/podlodkacast/
Twitter-аккаунт: https://twitter.com/PodlodkaPodcast
Ведущие в выпуске:
Катя Петрова, Стас Цыганов
Полезные ссылки:
Введение в верификацию в Coq https://softwarefoundations.cis.upenn.edu/
Комплятор C верифицированный в Coq
https://compcert.org/
Книжка Лампорта по спецификации сисатем https://lamport.azurewebsites.net/tla/book-02-08-08.pdf
Facebook Infer, анализ построенный на логике
https://fbinfer.com/
Как в Амазоне используют формальные методы
https://www.youtube.com/watch?v=YdxvOPenjWI&ab_channel=ACMSIGOPS
Model Checker для Rust
https://github.com/model-checking/kani
Сайт Ильи
https://ilyasergey.net
Twitter Ильи
https://twitter.com/ilyasergey