Лялямбда

школа верификации, компиляторов и реверса

’21

с элементами прикладного ФП

17/07-01/08
Новости→
Регистрация→
ГЛАВНОЕ РУССКОЯЗЫЧНОЕ СОБЫТИЕ ПО ВЕРИФИКАЦИИ ЭТОГО ЛЕТА

Конструктивная верификация, model checking, индустриальное компиляторостроение, реверс-инжиниринг железа с перерывами на спорт, лошадей, личностный рост, поход, музыку, танцы, йогу, бёрнинг мэн, шахматы, показ мод, хайкинг и фотографию.

Что программа?

Две недели

  1. Интенсив по прикладному ФП и пререквизитам воркшопов (вводный трек) и избранным темам с фронтира (продвинутый)

    По четыре пары. Основной формат – семинары. Методички, домашки и чат будут доступны для онлайн-участников.

  2. Тематические воркшопы: модальная теория типов, HOL, коиндуктивные типы в ТК, TLA…

    Каждый участник приезжает с чем-нибудь от lightning’а на пять минут до интенсива на три дня или воркшопа на пару пар. Приглашённые эксперты рассказывают о своих текущих исследованиях, а энтузиасты о том, как они тыкали в ФМ, что получилось, и как сделать так же и даже лучше.

    Воркшопы или интерактивные, про приобретение конкретных навыков (таких 80%), или про уточнение карты и представления о предмете (20%). Ниже список предварительных тем:

  3. Хакатон

    Чтобы приложить новоприобретённые скиллы на живых задачах. Двое суток с чекпоинтами.

В одном дне

В одном дне шесть пар, шесть воркшопов от участников: технических на заявленную тему, технических на другие темы (введение в восьмибитный AVR, сайтики на Purescript, круглый стол про лучший первый язык программирования), и нетехнических. Приезжайте с чем угодно, что будет востребованно и интересно и что можете классно рассказать: Вася проведёт MMA или тайский бокс, Слава пояснит за роль диалектического материализма в либертарианском мире, Маша научит трюкам с мячом, Алиса актёрскому мастерству, Кирилл привезёт домашний рецепт пельменей, а Даша покажет, как делать настойки.

(Во время интенсивов воркшопа два-три, а пары три или четыре.)

Каждый вечер выбираем программу на послезавтра.

Кто участники?

  1. Настоящие верификаторы, что на трансляторах собаку съели

  2. Сеньоры-помидорыsenior software developers с тягой к прекрасному

    Это необычная и сама по себе интересная предметная область, примерно как научиться программировать FPGA. Если вы занимаетесь прикладной разработкой (не R&D), вам могут не пригодиться обсуждаемые инструменты прямо: пока они недостаточно коммодитизированы. Тем не менее, некоторые концепции типа метапрограммирования через написание своего компилятора могут сильно упростить решение задач, а инструменты model checking и солверы, которые мы выделим в отдельный воркшоп, полезны широко и малоизвестны.

  3. Инженеры по компиляторами сочувствующие

    Когда делали CompCert, верифицированный компилятор C, нашли порядка 300 багов в GCC и clang. Здесь исследуем верифицированные трансформации, чтобы оптимизации композировались.

  4. Системные и embedded-программисты

    Когда мы научились верифицировать программы, начинает хотеться уменьшить Trusted Computing Base. Например, экстракцией в C, а не в OCaml, чтобы исключить рантайм. Или верификацией ОС. Или верификацией железа – в зависимости от критичности проекта. Здесь нужна работа не только инженера по доказательствам, но и специалиста по низкоуровневому. С другой стороны, синтез позволяет избежать большой ручной работы: так, вместо ручной оптимизации криптографического кода можно просто написать доказанный суперкомпилятор и быть быстрее всех.

  5. Эффективные альтруисты

    Формальная верификация стратегически интересна по Scale-Tractability-Neglectedness (не ЭА-peer-reviewed-мнение): выживая последние десятые процентов багов из всеми используемого ПО (ОС, драйвера, кодеки, криптография, прошивки контроллеров) можно получить мультипликативный импакт; за счёт механичности и композируемости можно изменить экономику V&V/QA.

  6. Студенты, студентки и их горящие глаза

    Эта школа – введение в необычное профессиональное направление; дядьки и тётьки, которые делают такие необычные вещи в продакшене; и лёгкая индустриальная и академическая профориентация.

Для верификаторов возможность поменторить, обменяться опытом, опробовать свои конструкции на помидорах, для помидоров и молодых скоростная прокачка в уникальной теме и сообщество, для всех нетворкинг, коммьюнити билдинг и ярко проведённое время.

Ниже – слайды с names & faces.

Площадка

Парк-отель “Ершово”, 60км от Москвы. Есть лес, пруд и поле, лодки, пинг-понг, бильярд и велосипеды, сауна и барбекю. Размещение двухместное или одноместное, питание пятиразовое. Три учебные аудитории на 50+ человек каждая, небольшие воркшопные и лекционный зал.

Можно добраться на общем автобусе, на машине, на электричке + автобусе или такси.

Яндекс.КартыЯндекс.Карты

Кому задавать вопросы?

Люди: names & faces

Хочу!

Чтобы попасть на школу, нужно пройти одноранговый отбор и оплатить оргвзнос.

Отбор

Отбор происходит так: вы заполняете опросник, которым продаёте себя, свои интересы и воркшопы другим участникам. Отослав его, вы получите в ответ несколько анкет других участников и сможете их лайкнуть – или дизлайкнуть.

Так (и из приглашённых спикеров) получается состав участников и воркшопов.

Заполнить форму регистрации и опросник!

Про деньги

Есть два раза, когда нужно кому-то заплатить:

  1. Оплачиваете проживание площадке напрямую
  2. Вносите оргвзнос за общие мероприятия, аренду аудиторий, работу организаторов

Если ваше участие оплачивает работодатель, будем рады, если вы возьмёте корпоративный билет – так у нас будет больше ресурсов на гранты.

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

Школа ведёт прозрачную бухгалтерию.

И после

Мы созваниваемся с вами на полчаса, чтобы ответить на любые вопросы по школе и познакомиться; заключаем с вами договор, по которому вы оплачиваете взнос; добавляетесь в пиплбук – и вы счастливый зарегистрированный участник!