Статьи в журналах
Статьи в сборниках
Тезисы докладов
Книги
Доклады на научных конференциях
НИР и НИОКР
Свидетельства о регистрации прав на программное обеспечение
Участие в редколлегии сборников
Участие в программных комитетах конференций
Руководство диссертациями
Авторство учебных курсов
Преподавание учебных курсов
–
Статьи в журналах
-
-
- 2019 Поиск конфликтов доступа к данным в HDL-описаниях
- Камкин А.С., Лебедев М.С., Смолов С.А.
- в журнале Труды Института системного программирования РАН (электронный журнал), том 31, № 3, с. 135-144
-
- 2018 Генератор тестовых программ для архитектуры RISC-V на основе инструмента MicroTESK
- Камкин А.С., Проценко А.С., Смолов С.А., Татарников А.Д.
- в журнале Проблемы разработки перспективных микро- и наноэлектронных систем МЭС, издательство Институт проблем проектирования в микроэлектронике РАН (Москва), том 2, с. 2-8
-
- 2018 MicroTESK: A Tool for Constrained Random Test Program Generation for Microprocessors
- Kamkin Alexander, Tatarnikov Andrei
- в журнале Lecture Notes in Computer Science, том 10742, с. 387-393 DOI
-
- 2017 MicroTESK: Specification-Based Tool for Constructing Test Program Generators
- Chupilko M., Kamkin A., Kotsynyak A., Tatarnikov A.
- в журнале Lecture Notes in Computer Science, том 10629, с. 217-220
-
- 2017 Генерация тестов для цифровой аппаратуры на основе высокоуровневых моделей
- Чупилко М.М., Камкин А.С., Лебедев М.С., Смолов С.А.
- в журнале Труды Института системного программирования РАН (электронный журнал), том 29, № 4, с. 247-256 DOI
-
- 2016 Метод масштабируемой верификации Promela-моделей протоколов когерентности кэш-памяти
- Буренков В.С., Камкин А.С.
- в журнале Проблемы разработки перспективных микро- и наноэлектронных систем МЭС, издательство Институт проблем проектирования в микроэлектронике РАН (Москва), с. 54-60
-
-
- 2016 Генератор тестовых программ для архитектуры ARMv8 на основе инструмента MicroTESK
- Камкин А.С., Коцыняк А.М., Проценко А.С., Татарников А.Д., Чупилко М.М.
- в журнале Труды Института системного программирования РАН (электронный журнал), том 28, № 6, с. 87-102 DOI
-
- 2016 Specification-Based Test Program Generation for MIPS64 Memory Management Units
- Kamkin A., Kotsynyak A.
- в журнале Труды Института системного программирования РАН (электронный журнал), том 28, № 4, с. 99-114 DOI
-
- 2016 Checking Parameterized PROMELA Models of Cache Coherence Protocols
- Burenkov V., Kamkin A.
- в журнале Труды Института системного программирования РАН (электронный журнал), том 28, № 4, с. 57-76 DOI
-
- 2015 Метод построения расширенных конечных автоматов по HDL-описанию на основе статического анализа кода
- Смолов С.А., Камкин А.С.
- в журнале Научно-технические ведомости Санкт-Петербургского государственного политехнического университета. Информатика. Телекоммуникации. Управление, издательство Федеральное государственное автономное образовательное учреждение высшего образования "Санкт-Петербургский политехнический университет Петра Великого" (Санкт-Петербург), с. 60-73
-
-
- 2015 Предисловие
- Камкин А.С., Петренко А.К., Терехов А.Н.
- в журнале Труды Института системного программирования РАН (электронный журнал), том 27, № 3, с. 7-8 DOI
-
- 2015 Проецирование систем переходов: преодоление комбинаторного взрыва при верификации параллельных систем
- Камкин А.С.
- в журнале Программирование, том 41, № 6, с. 53-71
-
- 2015 Метод построение тестового оракула для подсистемы памяти многоядерного микропроцессора на основе недетерминированной функциональной модели
- Камкин А.С., Петроченков М.В.
- в журнале Вопросы радиоэлектроники, том 3, № 3, с. 84-95
-
- 2015 Projecting Transition Systems: Overcoming State Explosion in Concurrent System Verification
- Kamkin A.S.
- в журнале Programming and Computer Software, издательство Pleiades Publishing, Ltd (Road Town, United Kingdom), том 41, № 6, с. 311-324 DOI
-
- 2015 An Extended Finite State Machine-Based Approach to Code Coverage-Directed Test Generation for Hardware Designs
- Melnichenko I., Kamkin A., Smolov S.
- в журнале Труды Института системного программирования РАН (электронный журнал), том 27, № 3, с. 161-182 DOI
-
- 2015 A Model-Based Approach to Design Test Oracles for Memory Subsystems of Multicore Microprocessors
- Kamkin A., Petrochenkov M.
- в журнале Труды Института системного программирования РАН (электронный журнал), том 27, № 3, с. 149-160 DOI
-
- 2015 An Approach to Test Program Generation Based on Formal Specifications of Caching and Address Translation Mechanisms
- Kamkin A., Protsenko A., Tatarnikov A.
- в журнале Труды Института системного программирования РАН (электронный журнал), том 27, № 3, с. 125-138 DOI
-
- 2014 Проверка корректности поведения HDL-моделей цифровой аппаратуры на основе динамического сопоставления трасс
- Иванников В.П., Камкин А.С., Чупилко М.М.
- в журнале Научно-технические ведомости Санкт-Петербургского государственного политехнического университета. Информатика. Телекоммуникации. Управление, издательство Федеральное государственное автономное образовательное учреждение высшего образования "Санкт-Петербургский политехнический университет Петра Великого" (Санкт-Петербург), с. 130-142
-
- 2014 Средства функциональной верификации микропроцессоров
- Камкин А.С., Коцыняк А.М., Смолов С.А., Татарников А.Д., Чупилко М.М., Сортов А.А.
- в журнале Труды Института системного программирования РАН (электронный журнал), том 26, с. 149-200
-
-
- 2014 Система поддержки верификации реализаций протоколов когерентности с использованием формальных методов
- Камкин А.С., Петроченков М.В.
- в журнале Вопросы радиоэлектроники, том 4, с. 27-38
-
- 2014 Расширяемая среда генерации тестовых программ для микропроцессоров
- Камкин А.С., Сергеева Т.И., Смолов С.А., Татарников А.Д., Чупилко М.М.
- в журнале Программирование, том 40, с. 3-14
-
- 2014 Extensible environment for test program generation for microprocessors
- Kamkin A.S., Sergeeva T.I., Smolov S.A., Tatarnikov A.D., Chupilko M.M.
- в журнале Programming and Computer Software, издательство Pleiades Publishing, Ltd (Road Town, United Kingdom), том 40, № 1, с. 1-9
-
- 2013 Трудности модульной верификации аппаратуры на примере буфера команд микропроцессора «Эльбрус-2s»
- Баратов Р.А., Камкин А.С., Майорова В.М., Мешков А.Н., Якушева М.А., Сортов А.А.
- в журнале Вопросы радиоэлектроники, том 4, с. 84-96
-
- 2011 Survey of modern technologies of simulation-based verification of hardware
- Kamkin A.S., Chupilko M.M., Petrenko A.K.
- в журнале Programming and Computer Software, издательство Pleiades Publishing, Ltd (Road Town, United Kingdom), том 37, № 3, с. 147-152
-
-
-
-
-
-
- 2007 The use of contract specifications for representing requirements and for functional testing of hardware models
- Ivannikov V.P., Kamkin A.S., Kossatchev A.S., Kuliamin V.V., Petrenko A.K.
- в журнале Programming and Computer Software, издательство Pleiades Publishing, Ltd (Road Town, United Kingdom), том 33, № 5, с. 272-282 DOI
Статьи в сборниках
-
-
-
- 2020 Deductive Binary Code Verification Against Source-Code-Level Specifications
- Kamkin Alexander, Khoroshilov Alexey, Kotsynyak Artem, Putro Pavel
- в сборнике Tests and Proofs. TAP 2020, серия Lecture Notes in Computer Science, издательство Springer International Publishing AG (Cham, Switzerland), том 12165, с. 43-58 DOI
-
- 2016 ESL Design with RTL-Verified Predesigned Abstract Communication Channels
- Haghi Najafi H., Chupilko M., Kamkin A., Navabi Z.
- в сборнике Proceedings of East-West Design & Test Symposium DOI
-
- 2016 Testing Logic Circuits at Different Abstraction Levels: An Experimental Evaluation
- Smolov S., Lopez J., Kushik N., Yevtushenko N., Chupilko M., Kamkin A.
- в сборнике Proceedings of East-West Design & Test Symposium DOI
-
-
- 2016 Universal Mitigation of NBTI-Induced Aging by Design Randomization
- Jenihhin M., Kamkin A., Navabi Z., Sadeghi-Kohan S.
- в сборнике Proceedings of East-West Design & Test Symposium DOI
-
-
- 2015 Specification-Based Test Program Generation for ARM VMSAv8-64 Memory Management Units
- Chupilko Mikhail, Kamkin Alexander, Kotsynyak Artem, Protsenko Alexander, Smolov Sergey, Tatarnikov Andrei
- в сборнике 2015 16th International Workshop on Microprocessor and SOC Test and Verification (MTV), место издания Institute of Electrical and Electronics Engineers (IEEE), с. 1-6 DOI
-
- 2013 Correctness checking of HDL-model behavior based on runtime trace matching
- Ivannikov V.P., Kamkin A.S., Chupilko M.M.
- в сборнике Tools and Methods of Program Analysis, TMPA 2013; Kostroma; Russian Federation; 10 October 2013 through 12 October 2013; Category numberP5172; Code 115685, место издания Institute of Electrical & Electronics Engineers (IEEE), с. 25-30 DOI
-
- 2013 Static analysis of HDL descriptions: Extracting models for verification
- Kamkin Alexander, Smolov Sergey, Melnichenko Igor
- в сборнике Proceedings of IEEE East-West Design&Test Symposium (EWDTS’2013), серия Symposium EWDTS, издательство Institute of Electrical and Electronics Engineers (Piscataway, NJ, United States)
-
- 2013 Проверка корректности поведения HDL-моделей цифровой аппаратуры на основе динамического сопоставления трасс
- Иванников В.П., Камкин А.С., Чупилко М.М.
- в сборнике Труды Конференции TMPA, место издания Кострома
-
- 2011 Simulation-based hardware verification with time-abstract models
- Kamkin Alexander
- в сборнике 2011 9th East-West Design & Test Symposium (EWDTS), серия Symposium EWDTS, издательство Institute of Electrical and Electronics Engineers (Piscataway, NJ, United States)
-
-
Тезисы докладов
-
- 2018 Формальная проверка эквивалентности описаний цифровой аппаратуры
- Смолов С.А., Камкин А.С., Лебедев М.С.
- в сборнике Новые информационные технологии в исследовании сложных структур: материалы Двенадцатой конференции с международным участием, место издания Издательский Дом Томского государственного университета Томск, тезисы, с. 83-84
-
- 2016 АВТОМАТИЧЕСКАЯ ГЕНЕРАЦИЯ ТЕСТОВ ДЛЯ ОПИСАНИЙ ЦИФРОВОЙ АППАРАТУРЫ НА ОСНОВЕ ПРОВЕРКИ МОДЕЛЕЙ С ПОМОЩЬЮ ИНСТРУМЕНТА NUXMV
- Камкин А.С., Смолов А.С., Лебедев М.С.
- в сборнике НОВЫЕ ИНФОРМАЦИОННЫЕ ТЕХНОЛОГИИ В ИССЛЕДОВАНИИ СЛОЖНЫХ СТРУКТУР, место издания Томск, тезисы, с. 50-51
Книги
- 2018 Введение в формальные методы верификации программ: учебное пособие
- Камкин А.С.
- издательство ООО "МАКС Пресс" (Москва) , ISBN 978-5-317-05767-1, 272 с.
Доклады на научных конференциях
-
- 2019 Extracting Assertions for Conflicts in HDL Descriptions (Устный)
- Авторы: Alexander Kamkin, Sergey Smolov, Mikhail Lebedev
- Spring/Summer Young Researchers' Colloquium on Software Engineering - 2019, Саратов, Russia, 29-31 мая 2019
-
- 2018 MicroTESK: Automated Architecture Validation Suite Generator for Microprocessors (Устный)
- Авторы: Chupilko M., Kamkin A., Protsenko A., Smolov S., Tatarnikov A.
- Design and Verification Conference and Exhibition Europe (DVCon Europe), Мюнхен, Germany, 24-25 октября 2018
-
- 2018 Автоматизация верификации микропроцессоров на основе формальных спецификаций системы команд (Пленарный)
- Автор: Камкин А.С.
- Новые информационные технологии в исследовании сложных структур, Алтайский край, п. Катунь, Russia, 4-8 июня 2018
-
- 2018 Test Program Generator MicroTESK for RISC-V (Стендовый)
- Авторы: Chupilko M., Kamkin A., Tatarnikov A., Protsenko A., Smolov S., Kotsynyak A.
- RISC-V Workshop, Барселона, Spain, 7-10 мая 2018
-
- 2018 Specification-Based Construction of Online TPGs for Microprocessors (Стендовый)
- Авторы: Chupilko M., Kamkin A.
- Design, Automation, and Test in Europe (DATE), University Booth, Дрезден, Germany, 19-23 марта 2018
-
- 2017 MicroTESK: Specification-Based Tool for Constructing Test Program Generators (Стендовый)
- Авторы: Kotsynyak A., Chupilko M., Kamkin A., Tatarnikov A.
- Haifa Verification Conference, Хайфа, Israel, 13-15 ноября 2017
-
- 2017 Создание генератора тестовых программ для микропроцессоров с архитектурой MIPS с помощью инструмента MicroTESK (Устный)
- Автор: Камкин А.С.
- Nano and Giga Challenges in Electronics, Photonics and Renewable Energy, Digital Design and Computer Architecture in the Era of System on Chip and Internet of Things, Томск, Russia, 18-22 сентября 2017
-
- 2017 Combining MicroTESK and SPIN for Verification of Multi-core Microprocessors (Стендовый)
- Авторы: Chupilko M., Kamkin A., Lebedev M., Tatarnikov A.
- Design, Automation, and Test in Europe (DATE), University Booth, Лозанна, Switzerland, 27-30 марта 2017
-
- 2016 Universal Mitigation of NBTI-Induced Aging by Design Randomization (Устный)
- Авторы: Jenihhin M., Sadeghi-Kohan S., Navabi Z., Kamkin A.
- East-West Design & Test Symposium, Ереван, Armenia, 14-17 октября 2016
-
- 2016 Формальная верификация аппаратуры: задачи и методы (Приглашенный)
- Автор: Камкин А.С.
- Проблемы разработки перспективных микро- и наноэлектронных систем, Москва, Russia, 3-7 октября 2016
-
- 2016 Specification-Based Test Program Generation for MIPS64 Memory Management Units (Устный)
- Авторы: Kamkin Alexander, Kotsynyak Artem
- X Международная конференция молодых ученых в области программной инженерии SYRCoSE, Московская область, Можайский район, деревня Красновидово, Russia, 30 мая - 1 июня 2016
-
- 2015 Specification-Based Test Program Generation for ARM VMSAv8-64 Memory Management Units (Устный)
- Авторы: Chupilko M., Kotsynyak Artem, Protsenko A., Smolov S., Tatarnikov A., Kamkin A.
- 16th International Workshop on Microprocessor Test and Verification (MTV 2015), Остин, United States, 3-4 декабря 2015
НИР и НИОКР
-
- 1 января 2011 - 31 декабря 2015 Теоретические основы и методы анализа и проектирования программ
- Кафедра системного программирования
- Руководитель: Иванников В.П. Ответственный исполнитель: Корухова Л.С. Участники НИР: Карпов Л.Е., Хорошилов А.В., Гайсарян С.С., Притула М.Н., Корныхин Е.В., Крюков В.А., Шарыгин Е.Ю., Малышко В.В., Кулямин В.В., Иванишин В.А., Клеменков П.А., Гомзин А.Г., Теймуразов К.Б., Федоренко Д.Г., Кузьменкова Е.А., Соловьев М.А., Бахтин В.А., Морозов С.В., Андрианов И.А., Маллачиев К.А., Кошелев В.К., Камкин А.С., Батузов К.А., Горемыкин О.В., Серебряков В.А., Мандрыкин М.У., Белеванцев А.А., Тарлапан О.А., Аветисян А.И., Буздалов Д.В., Шуберт А.В., Падарян В.А., Меркулов А.П., Кузнецов К.А., Петренко А.К., Кузнецов С.Д., Турдаков Д.Ю., Вартанов С.П., Алексиянц А.В., Посконин А.В., Дудина И.А.
Свидетельства о регистрации прав на программное обеспечение
-
- 2018 Программная модель архитектуры RISC-V (SOFT)
- Авторы: Камкин А.С., Проценко А.С., Татарников А.Д.
- #2018663565, 31 октября
-
- 2018 Программа динамической модульной верификации описаний цифровой аппаратуры C++TESK Testing Toolkit (SOFT)
- Авторы: Камкин А.С., Пакулин Н.В., Проценко А.С., Сортов А.А., Чупилко М.М.
- #2018663567, 31 октября
-
- 2018 Retrascope: Программа анализа HDL-описаний цифровой аппаратуры (SOFT)
- Авторы: Камкин А.С., Лебедев М.С., Мельниченко И.В., Проценко А.С., Смолов С.А., Чупилко М.М.
- #2018663000, 18 октября
-
- 2017 Fortress: Набор модулей для описания и преобразования формул и разрешения ограничений (SOFT)
- Авторы: Камкин А.С., Татарников А.Д., Коцыняк А.М., Смолов С.А.
- #2017660813, 27 сентября
Участие в редколлегии сборников
Участие в программных комитетах конференций
-
- 30 мая - 1 июня 2018 XII Международная конференция молодых ученых в области программной инженерии SYRCoSE
- Член программного комитета
- Великий Новгород, Russia
-
- 3-4 марта 2017 Tools and Methods of Program Analysis Conference (TMPA)
- Член программного комитета
- Москва, Russia
-
- 31 мая - 1 июня 2017 Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE)
- Член программного комитета
- Иннополис, Russia
-
- 30 мая - 1 июня 2016 X Международная конференция молодых ученых в области программной инженерии SYRCoSE
- Член программного комитета
- Московская область, Можайский район, деревня Красновидово, Russia
-
- 30 мая - 1 июня 2016 X Международная конференция молодых ученых в области программной инженерии SYRCoSE
- Член организационного комитета
- Московская область, Можайский район, деревня Красновидово, Russia
-
- 12-14 ноября 2015 Третья международная научно-практическая конференция TMPA-2015
- Член программного комитета
- Санкт-Петербург, Russia
-
- 28-30 мая 2015 9th Spring/Summer Young Researchers' Colloquium on Software Engineering
- Член организационного комитета
- Самара, Russia
Руководство диссертациями
-
- 2017 Автоматизация конструирования генераторов тестовых программ для микропроцессоров на основе формальных спецификаций
- Кандидатская диссертация по специальности 05.13.11 - Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей (техн. науки)
- Автор: А.Д. Татарников
- Научный руководитель: Камкин А.С., к.ф.-м.н., МГУ имени М.В. Ломоносова
- Защищена в совете Д 002.087.01 при ИСП РАН
- Организация, в которой выполнялась работа: Федеральное государственное бюджетное учреждение науки Институт системного программирования им. В.П. Иванникова Российской академии наук
- Ведущая организация: АО "МЦСТ"
- Оппоненты: Лацис А.С., Чибисов П.А.
Авторство учебных курсов
Преподавание учебных курсов
-
- с 12 февраля 2016 Верификация моделей программ
- МГУ имени М.В. Ломоносова, Факультет вычислительной математики и кибернетики, Кафедра системного программирования
- обязательная, вариативной части, лекции, 108 часов