Правильный подкаст для IT-шников
…
continue reading
Контент предоставлен Podlodka Podcast, Егор Толстой, Стас Цыганов, Екатерина Петрова, and Евгений Кателла. Весь контент подкастов, включая выпуски, графику и описания подкастов, загружается и предоставляется непосредственно Podlodka Podcast, Егор Толстой, Стас Цыганов, Екатерина Петрова, and Евгений Кателла или его партнером по платформе подкастов. Если вы считаете, что кто-то использует вашу работу, защищенную авторским правом, без вашего разрешения, вы можете выполнить процедуру, описанную здесь https://ru.player.fm/legal.
Player FM - приложение для подкастов
Работайте офлайн с приложением Player FM !
Работайте офлайн с приложением Player FM !
Podlodka #268 – Формальные методы и верификация программ
MP3•Главная эпизода
Manage episode 329545587 series 2529307
Контент предоставлен Podlodka Podcast, Егор Толстой, Стас Цыганов, Екатерина Петрова, and Евгений Кателла. Весь контент подкастов, включая выпуски, графику и описания подкастов, загружается и предоставляется непосредственно Podlodka Podcast, Егор Толстой, Стас Цыганов, Екатерина Петрова, and Евгений Кателла или его партнером по платформе подкастов. Если вы считаете, что кто-то использует вашу работу, защищенную авторским правом, без вашего разрешения, вы можете выполнить процедуру, описанную здесь https://ru.player.fm/legal.
Мечтаете, чтобы ваше ПО было сверх надежным, но грустите, ведь даже самый большой набор тестов не гарантирует 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
…
continue reading
378 эпизодов
MP3•Главная эпизода
Manage episode 329545587 series 2529307
Контент предоставлен Podlodka Podcast, Егор Толстой, Стас Цыганов, Екатерина Петрова, and Евгений Кателла. Весь контент подкастов, включая выпуски, графику и описания подкастов, загружается и предоставляется непосредственно Podlodka Podcast, Егор Толстой, Стас Цыганов, Екатерина Петрова, and Евгений Кателла или его партнером по платформе подкастов. Если вы считаете, что кто-то использует вашу работу, защищенную авторским правом, без вашего разрешения, вы можете выполнить процедуру, описанную здесь https://ru.player.fm/legal.
Мечтаете, чтобы ваше ПО было сверх надежным, но грустите, ведь даже самый большой набор тестов не гарантирует 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
…
continue reading
378 эпизодов
Все серии
×Добро пожаловать в Player FM!
Player FM сканирует Интернет в поисках высококачественных подкастов, чтобы вы могли наслаждаться ими прямо сейчас. Это лучшее приложение для подкастов, которое работает на Android, iPhone и веб-странице. Зарегистрируйтесь, чтобы синхронизировать подписки на разных устройствах.