• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Articles
  • Об интеграции формальных методов в задачах верификации операционных систем
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Priority areas
  • business informatics
  • economics
  • engineering science
  • humanitarian
  • IT and mathematics
  • law
  • management
  • mathematics
  • sociology
  • state and public administration
by year
  • 2027
  • 2026
  • 2025
  • 2024
  • 2023
  • 2022
  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011
  • 2010
  • 2009
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
  • 1999
  • 1998
  • 1997
  • 1996
  • 1995
  • 1994
  • 1993
  • 1992
  • 1991
  • 1990
  • 1989
  • 1988
  • 1987
  • 1986
  • 1985
  • 1984
  • 1983
  • 1982
  • 1981
  • 1980
  • 1979
  • 1978
  • 1977
  • 1976
  • 1975
  • 1974
  • 1973
  • 1972
  • 1971
  • 1970
  • 1969
  • 1968
  • 1967
  • 1966
  • 1965
  • 1964
  • 1963
  • 1958
  • More
Subject
News
June 3, 2026
Creative Work as a Remedy for Burnout
The creative, supportive atmosphere and innovative methods at the Centre for Sociocultural Research make it appealing to early-career scholars. Over years of working at HSE University, they grow into researchers and lecturers recognised both in Russia and abroad. Chief Research Fellow Zarina Lepshokova and Leading Research Fellow Ekaterina Bushina spoke about their journey at the centre and at HSE, their research, and the role of mentors in their academic success.
June 2, 2026
HSE Study Reveals Imbalance in the Generative AI Market
Researchers at HSE University analysed how effectively the global generative artificial intelligence market converts investment into real revenue, concluding that AI is currently developing faster than it is paying off. The results have been published in the journal Foresight and STI Governance.
June 2, 2026
Discovering Science through Russian Language: HSE Prep Year Students Present at International Conference in Kazan
On May 23, 2026, the V International Scientific and Practical Conference ‘Discovering the World of Science’ took place in Kazan at the Preparatory Faculty for International Students of Kazan Federal University. Four students of the HSE International Preparatory Year took part in the event: two delivered their presentations in person, while two participated online. Their work was supervised by Acting Director of the International Prep Year Irina Isaeva and lecturer Ekaterina Kozhemyakova.

 

Have you spotted a typo?
Highlight it, click Ctrl+Enter and send us a message. Thank you for your help!

Publications
  • Books
  • Articles
  • Chapters of books
  • Working papers
  • Report a publication
  • Research at HSE

?

Об интеграции формальных методов в задачах верификации операционных систем

Труды Института системного программирования РАН. 2015. Т. 27. № 5. С. 175–190.
Petrenko A. K., Kuliamin V., Khoroshilov A. V.
Language: Russian
DOI
Text on another site
Keywords: операционная систематестирование на основе моделейпроверка моделейдедуктивная верификацияинтеграция методов верификациипрограммные контракты
Similar publications
ВНЕДРЕНИЕ СВОБОДНОГО ПО НА ПРИМЕРЕ ПАКЕТА АЛЬТ В ИНФРАСТРУКТУРУ ИНЖЕНЕРНЫХ ОБРАЗОВАТЕЛЬНЫХ ПРОГРАММ УНИВЕРСИТЕТА МИЭМ НИУ ВШЭ
Starykh V., В кн.: Объединённая конференция «СПО: от обучения до разработки» : материалы конференции. Переславль-Залесский, 19–22 мая 2022 г.: М.: ООО «Макс Пресс», 2022. С. 46–47.
Russian operating systems are an integral part of the import substitution process. They are actively used in the public sector, where special requirements are imposed on the protection and processing of information, stability and compatibility of systems and applications used. Russian operating systems allow you to implement the full range of tasks without additional investments ...
Added: November 16, 2022
Объединённая конференция «СПО: от обучения до разработки» : материалы конференции. Переславль-Залесский, 19–22 мая 2022 г.
ООО «Макс Пресс», 2022.
The book contains the conference abstracts approved by the Program Committee of the joint conference "OSS: from training to development". ...
Added: November 16, 2022
Объединённая конференция «СПО: от обучения до разработки» : материалы конференции. Переславль-Залесский, 19–22 мая 2022 г.
М.: ООО «Макс Пресс», 2022.
Конференция объединяет два традиционных ежегодных мероприятия «Базальт СПО»: конференцию разработчиков свободных программ и конференцию «СПО в высшей школе». На дискуссионных площадках встречаются ведущие разработчики СПО из России и стран ближнего зарубежья, педагоги вузов и школ, которые используют свободные программы для проведения занятий, студенты и школьники, стремящиеся стать профессионалами в разработке СПО. Разработчики могут не только обсудить ...
Added: October 30, 2022
App Store: границы рынка и рыночная власть Apple
Павлова Н. С., Kurdin A., Поляков Д. А., Вестник Московского университета. Серия 6: Экономика 2021 № 1 С. 103–127
The article is based on the research in mobile applications markets. The distribution of market power in these markets depends on the ability of a digital ecosystem’s owner to control the handling of mobile applications inside the ecosystem. The degree of this control is determined by the substitutability of different application stores as necessary facilities ...
Added: July 2, 2021
InnoChain: распределенный реестр для индустриального применения с формальной верификацией на всех уровнях реализации
Кухаренко В. А., Зиборов К. В., Садыков Р. Ф. et al., Моделирование и анализ информационных систем 2020 Т. 27 № 4 С. 454–471
Степень применения методов формальной верификации в индустриальных проектах всегда была ограничена. Распространение систем распределенного реестра (СРР), известных также как блокчейн, быстро меняет ситуацию. Поскольку основной областью применения СРР является автоматизация финансовых транзакций, свойства предсказуемости и надежности являются критическими при реализации таких систем. Реальное поведение СРР определяется выбранным протоколом консенсуса, свойства которого нуждаются в строгой спецификации ...
Added: May 31, 2021
Using a bounded model checker for test generation: How to kill two birds with one SMT solver
Beliaev Mikhail, Petrov M., Gagarski K. et al., Automatic Control and Computer Sciences 2015 Vol. 7 No. 49 P. 466–472
Added: July 3, 2019
Компонентная верификация операционных систем
Kuliamin V., Petrenko A. K., Khoroshilov A. V., Труды Института системного программирования РАН 2018 Т. 30 № 6 С. 367–382
В работе рассматриваются полученные недавно результаты на пути к полномасштабной верификации промышленно используемых операционных систем (ОС). Таковыми считаются не системы, разработанные в целях демонстрации определенной исследовательской идеи, а ОС, активно используемые в каких-то областях экономики и управленческой деятельности и развиваемые на протяжении значительного времени. Предлагается декомпозиция заявленной цели верификации промышленной ОС в целом на задачи ...
Added: February 14, 2019
Введение в формальные методы верификации программ: учебное пособие
Kamkin A., М.: МАКС Пресс, 2018.
This textbook is devoted to formal methods for program verification and is based on the lectures given by the author at CMC MSU, DCAM MIPT, and FCS HSE. It describes the basics of such approaches as deductive analysis and model checking. The list of topics includes formal semantics of programming languages (operational and axiomatic semantics), ...
Added: November 2, 2018
Эффекты распространения рыночной власти владельцев ключевых мощностей на рынках программного обеспечения
Shastitko A., Kurdin A., Управленец 2017 № 4 (68) С. 43–52
The article assesses the policies instituted by producers of operating systems, when they aim to boost sales of applied software integrated into their operating systems. It analyses the policies through the prism of the effects they exert on other participants of the markets for operating systems and applied software. To perform the analysis, the authors ...
Added: August 23, 2018
Основы операционных систем. Курс лекций. (Издание третье, дополненное и исправленное), ISBN 978-5-89155-301-9
Karpov V. E., Коньков К. А., Физматкнига, 2019.
Книга представляет собой систематизированный лекционный учебный курс по теории операционных систем. В ней рассмотрены фундаментальные принципы построения и особенности проектирования современных ОС. ...
Added: August 19, 2018
Верификация и анализ вариабельных операционных систем
Kuliamin V., Лаврищева Е. М., Мутилин В. С. et al., Труды Института системного программирования РАН 2016 Т. 28 № 3 С. 189–208
В данной работе рассматриваются проблемы верификации и анализа сложных операционных систем с учетом их вариабельности, или наличия большого количества разнообразных конфигураций. Исследуются методы, позволяющие преодолеть эти проблемы, проводится их обзор и классификация. Выделены классы методов, использующих для анализа инструменты, не учитывающие вариабельность, и выборки вариантов системы и методов, использующих специализированные инструменты, учитывающие вариабельность. Как наиболее ...
Added: August 28, 2017
Вариативность логистической составляющей бизнес-моделей металлургических предприятий России
Sterligova A., Лящук В. В., Логистика и управление цепями поставок 2016 № 1(72) С. 84–90
The article continues A.N. Sterligova’s publication “Logistical context of enterprise business model” (Logistics and Supply Chain Management. – №1 (66). – 2015. – pages 24-34). As it was described in that publication, in a challenging economic environment strategic changes for business can be implemented by changing their business models. The author provided a definition of ...
Added: April 15, 2016
СИСТЕМА ОБРАБОТКИ ЗАКАЗОВ КАК РЕЗЕРВ ПОВЫШЕНИЯ ЭФФЕКТИВНОСТИ ПРЕДПРИЯТИЯ
Chulanova G. Y., Известия высших учебных заведений. Технология легкой промышленности 2015 Т. 27 № 1 С. 48–54
В статье рассматривается построение и функционирование цикла управления заказом и выявлении слабых мест и разрывов в его работе. ...
Added: March 15, 2015
A Study of Cloud/IX Operating System for the ARM-based Data Center Server Platform
Leokhin, Y., Panfilov, P., Procedia Engineering 2015 Vol. 100 P. 1696–1705
Exponential growth in data production and a prominent trend in data center design architecture – a shift from expensive hardware towards a multitude of simple servers – pose new tasks and demand the use of different strategies for data center architects. In this work, a new solutions to distributed systems design are discussed, which are ...
Added: March 6, 2015
Отечественная операционная система Cloud/IX для серверов на процессорах архитектуры ARM
Ю.Л. Леохин, И.Н. Дворецкий, А.С. Мягков, Качество. Инновации. Образование 2014 Т. 113 № 10 С. 52–59
The article describes the main issues related to the development centers and storage, solutions, presented the domestic operating system Cloud / IX server processors architecture ARM, hello test results of http-server nginx ...
Added: March 6, 2015
  • About
  • About
  • Key Figures & Facts
  • Sustainability at HSE University
  • Faculties & Departments
  • International Partnerships
  • Faculty & Staff
  • HSE Buildings
  • HSE University for Persons with Disabilities
  • Public Enquiries
  • Studies
  • Admissions
  • Programme Catalogue
  • Undergraduate
  • Graduate
  • Exchange Programmes
  • Summer University
  • Summer Schools
  • Semester in Moscow
  • Business Internship
  • Research
  • International Laboratories
  • Research Centres
  • Research Projects
  • Monitoring Studies
  • Conferences & Seminars
  • Academic Jobs
  • Yasin (April) International Academic Conference on Economic and Social Development
  • Media & Resources
  • Publications by staff
  • HSE Journals
  • Publishing House
  • iq.hse.ru: commentary by HSE experts
  • Library
  • Economic & Social Data Archive
  • Video
  • HSE Repository of Socio-Economic Information
  • HSE1993–2026
  • Contacts
  • Copyright
  • Privacy Policy
  • Site Map
Edit