• 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
  • 2028
  • 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
September 25, 2026
AI Users Earn Up to 41.8% More Than Non-Users
Research conducted by economists at HSE University has revealed a significant correlation between the regular use of GenAI in the workplace and higher pay among Russian employees. The study found that individuals who frequently use GenAI in their professional activities earn notably more than those who reject these new tools or resort to them occasionally. The salary premium for highly qualified specialists reaches 41.8%. The article was published in the Voprosy Ekonomiki journal.
September 24, 2026
‘Feedback and Constructive Criticism Are Essential in Our Profession
Vincent Fardeau, Associate Professor at HSE ICEF, has reached a major career milestone: he recently published his paper ‘Asymmetric Thin Markets’ in the Journal of Financial Economics, successfully passed his major academic review, and received tenure. In this interview, Vincent discusses the story behind the paper, explains the concept of asymmetric thin markets, and shares his advice for young scholars aiming to publish in top-tier journals.
September 22, 2026
Personal Interest in Doctoral Thesis Topic Most Important for Confidence in Successful Defence
A researcher at HSE University analysed data on 1,539 doctoral students from 161 Russian universities to identify which features of a thesis topic are associated with academic success and engagement. The most important factor was found to be personal interest in the research topic, which was associated with almost all key aspects of doctoral programme experience—from engaging with the academic supervisor to research activity and confidence about successfully defending the thesis. The findings have been published in Higher Education.

 

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