Камкин Александр Сергеевич

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

Преподаёт дисциплины, напрямую выросшие из его исследовательской работы. Магистрантам факультета компьютерных наук направления «Программная инженерия» читает курс «Верификация программного обеспечения» — он же доступен магистрантам других программ в формате «Маго-лего». Студентам четвёртого курса бакалавриата МИЭМ по направлению «Информатика и вычислительная техника» читает «Высокоуровневое и имитационное моделирование цифровых систем». Курс по верификации ведёт непрерывно с 2021/2022 учебного года.

Научные интересы — программная и компьютерная инженерия, формальные методы, верификация программ и микропроцессоров, верификация моделей программ, тестирование на основе моделей, статический анализ. Ключевой прикладной результат — инструмент генерации тестовых программ для микропроцессоров MicroTESK, которому посвящена целая серия его публикаций: «MicroTESK: Specification-Based Tool for Constructing Test Program Generators» (2017), «MicroTESK: A Tool for Constrained Random Test Program Generation for Microprocessors» в серии Lecture Notes in Computer Science (2018), «Maintaining ISA Specifications in MicroTESK Test Program Generator» (2018) и «Test Program Generator MicroTESK for RISC-V» (2018). С архитектурой RISC-V связана и работа «Open-Source Validation Suite for RISC-V» (2019).

Второе направление — верификация программ и аппаратуры. Ему принадлежат работы «Deductive Binary Code Verification Against Source-Code-Level Specifications» (Lecture Notes in Computer Science, 2020) и обзорная статья «Survey of Modern Technologies of Simulation-Based Verification of Hardware» в журнале Programming and Computer Software (2011). Занимается сравнением открытых маршрутов проектирования цифровой аппаратуры: статьи «Comparison of Open Flows for Digital Hardware Development: qFlow, OpenLANE, Coriolis, and SymbiFlow» (2021) и «Comparison of High-Level Synthesis and Hardware Construction Tools» (2022) вышли в «Трудах Института системного программирования РАН». В 2024 году опубликовал работу об открытом промежуточном представлении на основе MLIR для проблемно-ориентированных потоковых вычислителей и статью о подходах к разрешению неоднозначностей при реконструкции треков заряженных частиц.

Регулярно публикуется в трудах международных конференций по тестированию и верификации аппаратуры — EWDTS, MTV, LATW, ICST. Среди его работ — статьи о генерации функциональных тестов для аппаратных проектов на основе расширенных конечных автоматов и проверки моделей, о применении параметризованной проверки моделей к реальным протоколам когерентности кэш-памяти, о генерации тестовых программ по спецификациям для блоков управления памятью ARM VMSAv8-64, о статическом анализе HDL-описаний и извлечении моделей для верификации. Доклад о MicroTESK представлял на Haifa Verification Conference в Хайфе (2017). Научные идентификаторы: ORCID 0000-0001-6374-8575, Scopus AuthorID 22135022900, ResearcherID B-2194-2014, SPIN РИНЦ 8587-2241. Владеет английским языком.