Хорошилов Алексей Владимирович

Доцент базовой кафедры «Системное программирование» Института системного программирования им. В.П. Иванникова РАН на факультете компьютерных наук НИУ ВШЭ, кандидат физико-математических наук (2006). В 2001 году окончил МГУ им. М.В. Ломоносова по специальности «Прикладная математика и информатика» с квалификацией «Математик. Системный программист». В Высшей школе экономики работает с 2015 года, научно-педагогический стаж — 21 год. Параллельно с 1999 года работает в Институте системного программирования РАН, где занимает позицию ведущего научного сотрудника, а с 2009 года преподаёт на кафедре системного программирования факультета вычислительной математики и кибернетики МГУ.

На факультете компьютерных наук читает магистрантам программной инженерии курс «Конструирование ядра операционных систем» — он же доступен студентам других программ в формате «маго-лего». Бакалаврам-программным инженерам четвёртого курса читал курс «Разработка операционных систем». Профессиональные интересы сосредоточены вокруг надёжности критически важного программного обеспечения: методы проектирования и разработки ответственных систем, формальные методы программной инженерии, методы верификации и валидации, тестирование на основе моделей, методы анализа требований.

В базе публикаций НИУ ВШЭ у него 29 работ, в реестре ORCID заявлена 51 работа. Значительная часть посвящена дедуктивной верификации системного кода. В статье «Deductive Binary Code Verification Against Source-Code-Level Specifications» (Lecture Notes in Computer Science, 2020) с соавторами показан подход к верификации бинарного кода против спецификаций уровня исходного текста. Работа «A Memory Model for Deductively Verifying Linux Kernel Module» (LNCS, 2018) описывает модель памяти для доказательной проверки модулей ядра Linux, а «Configurable toolset for static verification of operating systems kernel modules» (журнал «Программирование», 2015) — настраиваемый инструментарий статической верификации таких модулей.

Второе крупное направление — формальные модели безопасности операционных систем. Совместно с коллегами из ИСП РАН выпустил монографию «Моделирование и верификация политик безопасности управления доступом в операционных системах» («Горячая линия — Телеком», 2019). К этому же циклу относятся статьи «Formal Verification of OS Security Model with Alloy and Event-B» (Springer, 2014), «Интеграция мандатного и ролевого управления доступом и мандатного контроля целостности в верифицированной иерархической модели безопасности операционной системы» («Труды ИСП РАН», 2020) и «ADV_SPM — Формальные модели политики безопасности на практике» (2017). Отдельная линия работ связана с авиационной операционной системой реального времени JetOS и с управлением требованиями к ответственным системам: «Управление требованиями к ответственным системам. Обзор решений» («Труды ИСП РАН», 2019), «Runtime Verification of Operating Systems Based on Abstract Models» («Программирование», 2023).

Публикуется преимущественно в «Трудах Института системного программирования РАН», журнале «Программирование» (Programming and Computer Software) и сборниках Lecture Notes in Computer Science, участвует в семинарах памяти В.П. Иванникова (Ivannikov Memorial Workshop) и конференциях Actual Problems of Systems and Software Engineering. Среди работ последних лет — «CPALockator: Thread-Modular Analysis with Projections» (LNCS, 2021) об анализе многопоточных программ и «Мониторинг и тестирование на основе многоуровневых спецификаций программ» (2020). Владеет английским языком. Научные идентификаторы: ORCID 0000-0002-6512-4632, SPIN РИНЦ 3388-8074, Scopus AuthorID 54881742400, ResearcherID B-7780-2012.