Embedded Files
На данном соревновании победители будут объявлены по каждой номинации👇
1. Моделирование и предотвращение катастрофы китайских скоростных поездов методом Model Checking
1. Моделирование и предотвращение катастрофы китайских скоростных поездов методом Model Checking
Уровень: средний
Цель: Создать формальную модель системы управления поездами по заданию, построить требования, найти контрпример, нарушающий свойства и приводящий к столкновению поездов, предложить способы избегания такого рода проблем
Задание: будет открыто во время соревнований
Задачу предложили: Гаранина, Старолетов, Шошмина (исследователи из институтов и университетов)
2. TLA+: Temporal Logic of Actions + data structures (Лаборатория Касперского)
2. TLA+: Temporal Logic of Actions + data structures (Лаборатория Касперского)
Уровень: средний
Аннотация:
TLA+ - Temporal Logic of Actions + data structures - это формальный язык, разновидность модальной логики, который позволяет с математической точностью описывать системы и с математической строгостью и надёжностью доказывать их свойства. TLA+ широко используется для спецификаций многозадачных, конкурентных и распределённых систем.
Несмотря на кажущуюся сложность определения, TLA+ весьма простой для понимания формализм и лёгкий в освоении и применении. Поэтому тем, кто впервые знакомится с областью формальных спецификаций поведения систем, можно смело рекомендовать TLA+ как первый шаг в интересный и увлекательный мир model-checking.
Участникам предлагается разобраться в основах TLA+, ознакомиться с основами спецификации систем на этом языке и анализа их поведения в автоматизированных инструментах model-checking и попробовать свои силы в несложной, но интересной с практической точки зрения задаче по разрешению проблем синхронизации в распределённой работе.
Особых требований к знаниям участников нет, достаточно базовых знаний дискретной математики и матлогики.
Задание: будет открыто во время соревнований
Задачу предложили: Васил Дядов и Илья Щепетков (Лаборатория Касперского)
3. Пошаговое выведение свойств в Isabelle/HOL (Лаборатория Касперского)
3. Пошаговое выведение свойств в Isabelle/HOL (Лаборатория Касперского)
Уровень: начальный
Аннотация:
Задание посвящено формальному доказательству свойств функций, моделирующих реализацию работы со структурами данных. Для этого используется Isabelle/HOL, система доказательств теорем, используемая в различных областях, начиная от элементарной теории чисел и математического анализа до спецификации и доказательства корректности языков программирования и даже целых операционных систем в ведущих мировых университетах и организациях. При этом определения и утверждения о свойствах записываются на специальном языке, а Isabelle/HOL проверяет их корректность. Подготовительные материалы разработаны в предположении, что участники не имеют опыта работы с этой системой, и для выполнения задания предоставленных материалов будет достаточно. В то же время задание предполагает, что участники владеют базовыми знаниями по математической логике и простейшим структурам данных. Опыт функционального программирования не является обязательным, но может упростить понимание из-за отсутствия в языке доказательств побочных эффектов. Isabelle/HOL имеет очень мощные механизмы поиска доказательств, выгодно отличающие её от других подобных систем. Однако, чтобы сузить объём материала для изучения, задание не полагается на механизмы автоматизации. Более того, допустимые средства ограничены простейшими методами, чтобы приблизиться к ситуации, когда из-за сложности решаемой задачи система не всегда может сама найти доказательство, и приходится двигаться к нему пошагово вручную.
Задание: будет открыто во время соревнований
Задачу предложил: Александр Когтенков (Лаборатория Касперского)
4. Дедуктивная верификация с использованием Rocq (Coq) (Группа Астра)
4. Дедуктивная верификация с использованием Rocq (Coq) (Группа Астра)
Уровень: средний/сложный (несколько заданий)
Статические анализаторы пытаются автоматически установить некоторые свойства программ без их выполнения.
Статические анализаторы можно использовать по-разному, например:
- для поиска ошибок, совершаемых программистами;
- в качестве верификаторов, гарантирующих соответствие программы определенным свойствам.
При поиске ошибок анализ должен быть точным (слишком большое количество ложных срабатываний делает инструмент непригодным), однако не ожидается и не предоставляется гарантия обнаружения всех ошибок определенного класса. С другой стороны, при верификации программ корректность анализа имеет первостепенное значение: если анализатор не выдает предупреждений, программа должна быть свободна от класса отслеживаемых анализатором ошибок.
Наша задача – разработать корректный статический анализатор для простого императивного языка программирования. Для этого мы будем использовать абстрактную интерпретацию, а доказательство корректности осуществлять с помощью Rocq.
Задание: будет открыто во время соревнований
Задачу предложил: Тимофей Черганов (Группа Астра)
5. Дедуктивная верификация одного из первых в истории математики циклических алгоритмов из Древней Индии
5. Дедуктивная верификация одного из первых в истории математики циклических алгоритмов из Древней Индии
Уровень: средний
Цель: Дедуктивная верификация решателя квадратичных диофантовых уравнений, реализующего индийский метод, являющийся одним из первых в истории математики циклическим алгоритмом
Задание: будет открыто во время соревнований
Задачу предложил: Дмитрий Кондратьев (исследователь)
Page updated
Google Sites
Report abuse