Приглашаем всех желающих на открытую лекцию на тему "Моделирование семантики языка программирования в системах проверки доказательств, с приложениями к типам информационных потоков", которая состоится 20 декабря в 10:45 в ауд. 122/1.
Цель лекции - дать участникам представление об использовании интерактивных помощников по проверке доказательств, с приложениями к типам информационных потоков (Isabelle prover), и показать, как это можно использовать для моделирования семантики низкоуровнего языка программирования с возможными приложениями в области информационной безопасности. Будет представлено определение «высокоуровневого» императивного языка программирования, языка ассемблера и их компиляторов, а также показано, как проверить верность отладки и сборки средств разработки. Будет затронуто исследование системы особого типа, предназначенного для предотвращения незаконного обмена информацией, и как ее можно провести моделирование в помощнике по проверке доказательств, с приложениями к типам информационных потоков.
Читает лекцию Мартин Штрекер, PhD, доцент, университет Пола Сабатье (Тулуза III), Тулуза, Франция.
Далее студентов ожидает экскурсия по вузу, в частности знакомство с лабораторией «OpenStack Remote Security Laboratory» («RESELA»).