Формальная спецификация

VerifyThis это серия соревнования по верификации программ, которые проходят ежегодно с 2011 года. Сейчас проходит отбор задач для соревнования этого года, которое пройдет в рамках конференции ETAPS 6 и 7 апреля в Люксембурге. Как я понял нет никакого ограничения по инструментам для верификации и команда сама выбирает наиболее удобный, за прошлые года на сайте указаны инструменты, которые использовали победившие команды: Why3, mCRL2, Dafny, VeriFast. На скриншоте типичная задача с соревнования. https://www.pm.inf.ethz.ch/research/verifythis.html

Лампорт опубликовал черновик своей новой книги с предварительным названием "A Science of Concurrent Programs". Если "Specifying Systems" больше про использование TLA+, то эта книга рассказывает про научные принципы, лежащие в основе языка TLA+ и почему TLA+ такой, какой он есть. Лампорт предупреждает, что книга содержит много математики. Вообще Лампорт классно объясняет и если например выбирать книгу про TLA+ между Specifying Systems и Practical TLA+, то мой выбор будет за первой. Из новой книги я успел прочитать только первую главу и стиль написания Лампорт не поменял. https://lamport.azurewebsites.net/tla/science.pdf

TLA+ 2023 survey https://docs.google.com/forms/d/e/1FAIpQLScmEprc8WcXzNoRqYO8qeO8TS83FRlTrN2qYOCu8ORfoea6Gg/viewform

Два года назад мне посчастливилось поучаствовать в Летней школе Лялямбда. Это выездное мероприятие, посвященное изучению формальных методов (наверное в первую очередь это формальная верификация и спецификация) и функциональному программированию. В прошлом году, например, был недельный трек введения в формальную верификацию ПО с помощью автоматического прувера Coq, введение в функциональное программирование на Haskell и множество докладов по темам Летней школы. В промежутках между занятиями было много других активностей как например спортивные игры, развлекательные мероприятия, потому что сложно непрерывно потреблять большой объём новой информации. В прошлом году Школа проходила в доме отдыха Ершово, недалеко от Звенигорода. Вообщем, если кратко описывать Школу, то это возможность познакомиться с формальными методами в неформальной обстановке. Для меня Школа была возможностью познакомиться поближе с Coq и у меня получилось это сделать. Слово организаторам: "Друзья! Мы рады анонсировать новую школу — Лялямбда (https://lalambda.school/). 15-23 июля в получасе от Тбилиси пройдёт летняя школа сложного программирования и современного искусства «Лялямбда». День на школе — это семь пар: четыре пары курса и три арт-попурри. В этом году на школе будут курсы не только про формальные методы, странные логики спецификации и ФП, но и про стэйт оф зэ арт теории музыки и проектирование микропроцессоров. В арте будут перформансы и джемы, утренняя йога, лежать на пуфике и слушать музыку, стоять на руках, плавать под водой, танцевать хип-хоп или танго, гулять по берегу озера — можно выбирать. В этот раз мы в модном отеле на озере. Форма для регистрации - https://forms.gle/GFuJiGFA4VctHz178 Так же можно запросить грант https://forms.gle/3CAwn1e4xr77PVAd7), если он вам нужен, а здесь (https://forms.gle/euzLpsYSCq3KK8Rv8) подать курс, мы помогаем их готовить. Вопросики можно писать @lalambda_bot."

Proposing an IRTF Usable Formal Methods Research Group https://csperkins.org/research/protocol-standards/2022-11-30-usable-formal-methods/