Школа Лялямбда
202 subscribers
1 photo
16 links
Школа верификации, компиляторов и реверса с элементами прикладного ФП.

https://lalambda.school

Контакты: @AntonTrunov (программа школы), @Polina_Surr (все вопросы), @AliceGirla (все вопросы)
Download Telegram
to view and join the conversation
Мария Недяк (bi.zone, Томск).

Тема воркшопа: "Фаззинг - где и как его применять".

Пререквизиты: базовое понимание языков Си и/или Си++.

Что вы узнаете: как применять фаззинг, анализировать процесс фаззинга и улучшать его.

Мария профессионально пишет на Golang, использует фаззинг в исследовательских проектах, преподаёт школьникам ассемблер и Си. В свободное время смотрит сериалы, катается на велосипеде, занимается спортом.

#спикеры
Упс, только что узнали, что Виталий Худобахшов не сможет участвовать в школе :(
Даня Рогозин (Serokell, ИППИ РАН, Москва) проведёт не один, а целых три воркшопа!

Тема воркшопа №1: "Введение в модальную логику. Зачем расширять классическую логику ромбиками и квадратиками".
Пререквизиты: необходимый бекграунд будет дан.
Что вы узнаете: базовые системы модальных логик и семантику Крипке.

Тема воркшопа №2: "Введение во временную логику, или как ромбики и квадратики читать в терминах времени”.
Пререквизиты: предыдущий курс по модальной логике.
Что вы узнаете: семантику Крипке для временных логик и временную логику рациональных и/или действительных чисел.

Тема воркшопа №3: "Временная и динамическая логики. Логики в верификации программ”.
Пререквизиты: предыдущий курс по временной логике.
Что вы узнаете: основы модальных и временных логик программ и базовые основы model checking, использующие такие системы временной логики как LTL.


Даня участвует в разработке компилятора языка Haskell в компании Serokell, пишет диссертацию по модальной/алгебраической логике в лаборатории алгебры и теории чисел ИППИ РАН. Время от времени рисует абсурдистские картинки, изучает классическую английскую литературу, разбирается в джазе и классической музыке.

#спикеры
1 июля в 15:00 по мск
в рамках пре-школы состоится вебинар
Игоря Коннова на тему:

Apalache: symbolic model checker for TLA+

TLA+ -- формальный язык, предназначенный для спецификации всех видов
компьютерных систем. Системные архитекторы применяют TLA+ для описания
параллельных, распределенных и отказоустойчивых протоколов. Такие системы
обычно описываются на полуформальных языках в виде псевдокода или диаграмм
состояний. Мы применяем TLA+ для описания протоколов в экосистеме блокчейнов
Tendermint/Cosmos

В первой половине доклада мы рассмотрим принципы спецификации протоколов на
примере протокола обмена криптотокенами в системе Cosmos IBC. На основе примера
показывается подход к итеративной разработке протоколов с применением
верификатора моделей Apalache

Во второй половине доклада мы рассмотрим принципы работы Apalache. Apalache
транслирует спецификацию на языке TLA+ в систему логических ограничений на
языке SMTLIB и вызывает решатель Z3 для проверки ограничений.

Ссылка на zoom встречу будет опубликована в день события.
9.07 в 19:00 part 1
10.07 в 19:00 part 2
Состоится двухсерийный вебинар.
Денис Юричев будет рассказывать про SAT и SMT решатели, по своей книге "SAT/SMT by example"

Эксклюзивная возможность услышать материал из уст автора, известного своими работами https://beginners.re/ и https://sat-smt.codes

Ссылки на zoom встречи будут опубликованы в дни событий.
14.07 в 18:00 part 1
15.07 в 18:00 part 2
16.07 в 18:00 part 3
Состоится трехсерийный вебинар Алекса Грызлова, программиста-исследователя в IMDEA Software Institute (Мадрид), который занимается сепарационными логиками для многопоточности, также интересуется верификацией компиляторов и гибридных систем, формализацией арифметики и устройством пруф-ассистентов.

Тема вебинара:
"FCSL, или пишем составные доказательства для спинлоков"

Не секрет, что верификация целых программ сложнее верификации алгоритмов, т.к. вдобавок ко всем ньюансам, нужно дополнительно учитывать так называемую процедурную абстракцию - способность рассуждать об модулях программы как о "чёрных ящиках". Однако сепарационные логики, с помощью которых верифицируют императивные программы с алиасингом (т.е. ссылками на одно значение разными переменными) зачастую опускают именно процедурную абстракцию, что приводит к проблеме композиции доказательств.

Один из способов подобраться к решению этой проблемы - обратиться к интуициям и наработкам теории категорий и теории типов. FCSL - как раз такая разновидность сепарационной логики, "притворяющейся" теорией типов. В трех частях мы рассмотрим идеи FCSL на примерах доказательств для
1) последовательных программ, 2) многопоточных программ с критическими секциями и 3) многопоточных программ с неблокирующими примитивами.

Продолжительность каждой серии около 60 минут.

Ссылки на zoom встречи будут опубликованы в дни событий.
!!!ВНИМАНИЕ!!! Актуальная Ссылка на zoom* конференцию 1 серии Вебинара Дениса Юричева будет опубликована в ближайшее время
Внезапно! Школа стартует через неделю (17 июля) с интенсива по функциональному программированию, который проведёт Дмитрий Халанский (JetBrains, Санкт-Петербург).

Тема интенсива: "Введение в функциональное программирование".

Пререквизиты: От слушателей ожидается умение программировать.

Что вы узнаете: участники этого интенсива ознакомятся с повсеместно встречающимися понятиями функционального программирования — сопоставлением с образцом, функциями высшего порядка, алгебраическими типами данных и классами типов, ленью и энергичностью, функторами и аппликативными функторами и всяким другим. Полученные знания мы применим, реализовав полноценный (вместе с парсером и красивой печатью результата) интерпретатор лямбда-исчисления, способный к тому же автоматически определять тип поданного ему на вход выражения.

Дмитрий проводит практики по функциональному программированию и математической логике в магистратуре JetBrains на базе ИТМО и работает программистом в JetBrains, в команде, разрабатывающей библиотеки для языка Kotlin".

#интенсивы
По многочисленным просьбам завтра, 11.07 в 19:00 part 3
Денис Юричев
продолжит рассказывать про SAT и SMT решатели, по своей книге "SAT/SMT by example" Эксклюзивная возможность услышать материал из уст автора, известного своими работами https://beginners.re/ и https://sat-smt.codes

Ссылки на zoom встречи будут опубликована в день события
Привет. Скоро пройдёт GoTo — школа как наша, только шире и для школьников. То же одноранговое преподавание, любовь и стэйт оф зэ арт концепции для *будущего поколения*. Ищут кураторов проектов.

Пример проекта — 4D-змейка на Хаскелле за сутки хакатона. В проектах можно делать ФП, верификацию и построение компиляторов вволю. Ещё будут веб-сервисы и распределённые системы, инфобез и низкоуровневое программирование, алгоритмы и их приложения (с этим тоже можно помогать).

Движ в Подмосковье, сразу после нас — 02/08-14/08, на от пары дней до всех двух недель. Окромя пар можно доить коз, кататься на лошадках, собирать клубнику и гулять в лесу.

Научи школьников программировать *как правильно*! Приходи в goto! Пиши @omrigan!
Внимание: вебинар Алекса Грызлова переносится на завтра (16.07) в связи с личными обстоятельствами. Сегодня встречи не будет.
Завтра
16.07 в 15:00 part 2
16.07 в 18:00 part 3
Продолжится трехсерийный вебинар Алекса Грызлова программиста-исследователя в IMDEA Software Institute (Мадрид), который занимается сепарационными логиками для многопоточности, также интересуется верификацией компиляторов и гибридных систем, формализацией арифметики и устройством пруф-ассистентов.

Тема вебинара:
"FCSL, или пишем составные доказательства для спинлоков"

Не секрет, что верификация целых программ сложнее верификации алгоритмов, т.к. вдобавок ко всем ньюансам, нужно дополнительно учитывать так называемую процедурную абстракцию - способность рассуждать об модулях программы как о "чёрных ящиках". Однако сепарационные логики, с помощью которых верифицируют императивные программы с алиасингом (т.е. ссылками на одно значение разными переменными) зачастую опускают именно процедурную абстракцию, что приводит к проблеме композиции доказательств.

Один из способов подобраться к решению этой проблемы - обратиться к интуициям и наработкам теории категорий и теории типов. FCSL - как раз такая разновидность сепарационной логики, "притворяющейся" теорией типов. В трех частях мы рассмотрим идеи FCSL на примерах доказательств для
1) последовательных программ, 2) многопоточных программ с критическими секциями и 3) многопоточных программ с неблокирующими примитивами.

Продолжительность каждой серии около 60 - 80 минут.

Ссылки на zoom встречи будут опубликованы в день события.

Позже будет доступна видеозапись Вебинара на YouTube канале школы.
Денис Юричев. SAT и SMT решатели, по своей книге "SAT/SMT by example" 3 части
Видео:

https://youtu.be/4FiazaVfC-g
https://www.youtube.com/watch?v=47EsAeImH20
https://youtu.be/m5UuADk4HXc