Публикации

Избранные статьи

• Denis Efremov, Mikhail Mandrykin, Alexey Khoroshilov
  Deductive Verification of Unmodified Linux Kernel Library Functions
  8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part II.


• А.В. Хорошилов, И.В. Щепетков
  ADV_SPM — Формальные модели политики безопасности на практике
  Труды ИСП РАН, том 29, вып. 3, 2017. С. 43-56.


• Е.М. Новиков
  Развитие ядра операционной системы Linux
  Труды ИСП РАН, том 29, вып. 2, 2017. С. 77-96.


• П.С. Андрианов, В.С. Мутилин, А.В. Хорошилов
  Конфигурируемый метод поиска состояний гонок в операционных системах с использованием предикатных абстракций
  Труды ИСП РАН, том 28-6, 2016. С. 65-86.


• А.В. Цыварев, А.В. Хорошилов
  Использование симуляции сбоев при тестировании компонентов ядра ОС Linux
  Труды ИСП РАН, том 27-5, 2015. С. 157-174.


• П.С. Андрианов, В.С. Мутилин, А.В. Хорошилов
  Метод легковесного статического анализа для поиска состояний гонок
  Труды ИСП РАН, том 27-5, 2015. С. 87-116.


• И.С. Захаров, М.У. Мандрыкин, В.С. Мутилин, Е.М. Новиков, А.К. Петренко, А.В. Хорошилов
  Конфигурируемая система статической верификации модулей ядра операционных систем
  Труды ИСП РАН, том 26-2, 2014. С. 5-42.


• Е.А. Герлиц, В.В. Кулямин, А.В. Максимов, А.К. Петренко, А.В. Хорошилов, А.В. Цыварев
  Тестирование операционных систем
  Труды ИСП РАН, том 26-1, 2014. С. 73-108.


• И.С. Захаров, В.С. Мутилин, Е.М. Новиков, А.В. Хорошилов
  Моделирование окружения драйверов устройств операционной системы Linux
  Труды ИСП РАН, том 25, 2013. С. 85-112.


• М.У. Мандрыкин, В.С. Мутилин, А.В. Хорошилов
  Введение в метод CEGAR — уточнение абстракции по контрпримерам
  Труды ИСП РАН, том 24, 2013. С. 219-292.


• Е.М. Новиков
  Построение спецификаций программных интерфейсов в открытой системе покомпонентной верификации ядра Linux
  Труды ИСП РАН, том 24, 2013. С. 293-316.


• Д. Бейер, А.К. Петренко
  Верификация драйверов операционной системы Linux
  Труды ИСП РАН, том 23, 2012. С. 405-412.


• В.С. Мутилин, Е.М. Новиков, А.В. Хорошилов
  Анализ типовых ошибок в драйверах операционной системы Linux
  Труды ИСП РАН, том 22, 2012. С. 349-372.


• М.У. Мандрыкин, В.С. Мутилин, Е.М. Новиков, А.В. Хорошилов
  Обзор инструментов статической верификации Си программ в применении к драйверам устройств операционной системы Linux
  Труды ИСП РАН, том 22, 2012. С. 293-326.


• В.С. Мутилин, Е.М. Новиков, А.В. Страх, А.В. Хорошилов, П.Е. Швед
  Linux Driver Verification Architecture
  Труды ИСП РАН, том 20, 2011. С. 163-187.


• Vladimir Rubanov, Alexey Khoroshilov, Euegeny Shatokhin
  Automated Formal Testing of C API Using T2C Framework
  Proceedings of 3rd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Greece, 2008.


• Д.В. Силаков, В.В. Рубанов
  LSB Navigator – онлайн справочник для разработчиков Linux приложений
  Тезисы докладов V Конференции разработчиков свободных программ на Протве. – М.: Институт Логики, 2008. С. 36-39.


• В.В. Рубанов
  Стандартизация и тестирование как составляющие обеспечения безопасности ОС Linux
  Материалы XVII Общероссийской конференции «Методы и технические средства обеспечения безопасности информации», СПб.: Изд-во Политехнического университета, 2008.


• В.В. Рубанов, А.В. Хорошилов, Е.А. Шатохин
  T2C: технология автоматизированной разработки тестов базовой функциональности программных интерфейсов
  Труды ИСП РАН, том 14, часть 2, 2008. С. 65-82.


• В. Рубанов
  Linux Standard Base (LSB): “Single Linux” Specification and Support Infrastructure
  Тезисы докладов конференции "Software Engineering Conference Russia 2007", ноябрь 2007.


• В. Рубанов
  Стандарт Linux Standard Base (LSB): единая платформа разработки приложений для Linux
  Тезисы докладов I Конференции "Стандартизация информационных технологий и интероперабельность. СИТОП 2007", октябрь 2007.


• А. Хорошилов
  Формальное описание интерфейсов как средство улучшения интероперабельности
  Тезисы докладов I Конференции "Стандартизация информационных технологий и интероперабельность. СИТОП 2007", октябрь 2007.


• В. Кулямин, А. Петренко, В. Рубанов, А. Хорошилов
  Формализация интерфейсных стандартов и автоматическое построение тестов соответствия
  Software Engineering Conference Russia (SECR 2006), ноябрь 2006.


• А. Гриневич, В. Кулямин, Д. Марковцев, А. Петренко, В. Рубанов, А. Хорошилов
  Использование формальных методов для обеспечения соблюдения программных стандартов
  Труды ИСП РАН, том 10, 2006.


• А. Хорошилов
  Linux Standard Base: история успеха?
  Труды ИСП РАН, том 10, 2006.


• В. Кулямин
  Формальные подходы к тестированию математических функций
  Труды ИСП РАН, том 10, 2006.


• Victor V. Kuliamin, Nickolay V. Pakoulin, and Alexander K. Petrenko
  Practical Approach to Specification and
  Conformance Testing of Distributed Network Applications
  Доклад на 2-nd International Service Availability Symposium, Берлин, апрель 2005.


• А.В. Баранцев, И.Б. Бурдонов, А.В. Демаков, С.В. Зеленов, А.С. Косачев, В.В. Кулямин, В.А. Омельченко, Н.В. Пакулин, А.К. Петренко, А.В. Хорошилов
  Подход UniTESK к разработке тестов: достижения и перспективы
  Труды Института системного программирования РАН. Том 5, 2004.
  

Пресс-релизы и презентации

• И. Щепетков
  Using Refinement in Formal Development of OS Security Policy Model
  Доклад на семинаре Event-B Day 2018, Токио, Япония, 10 ноября, 2018.
  


• А. Хорошилов
  Proving sequential properties of unmodified Linux kernel code
  Доклад на семинаре Sound Static Analysis for Security Workshop 2018, Гейтерсберг, Мэриленд, США, 27-28 июня, 2018.
  


• А. Хорошилов
  ADV_SPM — Формальные модели политики безопасности на практике
  Доклад на конференции РусКрипто-2017, Москва, 21-24 марта 2017 г.


• П. Андрианов, В. Мутилин, А. Хорошилов
  Predicate Abstraction Based Configurable Method for Data Race Detection in Linux Kernel
  Доклад на 4-й международной конференции Инструменты и методы анализа программ, Москва, Россия, 3-4 марта 2017 г.
  


• А. Хорошилов, А. Цыварев
  Systematic Testing of Fault Handling Code in Linux Kernel
  Доклад на конференции Linux Plumbers Conference 2014, Дюссельдорф, Германия, 15 октября 2014 г.


• В. Мутилин, А. Хорошилов
  The Experience of Linux Driver Verification
  Доклад на Дагштульском семинаре №14171 Evaluating Software Verification Systems: Benchmarks and Competitions, Дагштуль, Германия. 25 апреля 2014 г.
  


• В. Мутилин
  Predicate Analysis with BLAST 2.7.1
  Доклад на 2-м международном соревновании по верификации программного обеспечения (SV-COMP-2013), Рим, Италия. 14 марта 2013 г.
  


• А. Хорошилов
  Linux Device-Drivers Verification Challenges
  Доклад на 2-м международном семинаре Linux Driver Verification, Ираклион, Греция. 15 октября 2012 г.
  


• Е. Новиков
  Using Aspect-Oriented Programming for Preparing C Programs for Static Verification
  Доклад на 2-м международном семинаре Linux Driver Verification, Ираклион, Греция. 15 октября 2012 г.
  


• М. Мандрыкин
  Pointer Analysis with Uninterpreted Functions
  Доклад на 2-м международном семинаре Linux Driver Verification, Ираклион, Греция. 15 октября 2012 г.
  


• А. Хорошилов
  The Experience of Heavy Weight Static Analysis of Linux Device Drivers
  Доклад на конференции Embedded World 2012, Нюренберг, Германия. 1 марта 2012 г.
  


• Е. Шатохин
  Использование динамического анализа для выявления проблем в модулях ядра
  Доклад на конференции LinuxCon Europe 2011, Прага, Чехия. 26-28 октября 2011 г.
  


• А. Хорошилов
  Linux Device Driver Verification Program
  Доклад на конференции LinuxCon Europe 2011, Прага, Чехия. 26-28 октября 2011 г.
  


• В. Рубанов
  Стандарт Linux Standard Base (LSB): единая платформа разработки приложений для Linux
  Доклад на конференции "Стандартизация информационных технологий и интероперабельность (СИТОП) 2007, 03 октября 2007 г.


• А.В. Хорошилов
  Формальное описание интерфейсов как средство улучшения интероперабельности
  Доклад на конференции "Стандартизация информационных технологий и интероперабельность (СИТОП) 2007, 03 октября 2007 г.


• А.К. Петренко
  Технология верификации программных интерфейсов
  Доклад на конференции LinuxWorld Moscow 2006, 04 сентября 2006 г.


• А. Гриневич, В. Кулямин, Д. Марковцев, А. Петренко, В. Рубанов, А. Хорошилов
  Formal Methods in Industrial Software Standards Enforcement
  Доклад на конференции Перспективы систем информатики (PSI'06), 27 июня 2006 г.


• А.К. Петренко
  UniTESK: технология тестирования на основе спецификаций
  Презентация на семинаре в IBM, 14 декабря 2005 г.


• ИСП РАН
  В России открывается Центр верификации ОС Linux
  Пресс-релиз, 12 октября 2005 г.

Дополнительная информация

Другие публикации и документы о технологии UniTESK и ее инструментах можно найти на сайте http://unitesk.ru/.