• 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
July 24, 2026
'Physics Is What the World Is Literally Built On'
Physicist Nina Dzhanayeva, recipient of a Vladimir Potanin Foundation scholarship, focuses her research on nanophotonics. In this interview for the HSE Young Scientists project, she discusses nanowells, scientific intuition, and how physics can help in making frangipane cream puffs.
July 20, 2026
Scientists Create Open Dataset for Studying Concentration
A team of Russian researchers, including scientists from HSE University–St Petersburg, has developed the first open multimodal dataset containing recordings of brain activity, heart function, and video observations to help researchers understand what happens in the human brain during deep concentration. In the future, the dataset could accelerate the development of neural interfaces, rehabilitation technologies, and AI systems. The article has been published in Scientific Data.
July 20, 2026
‘Science Is Universal-It Knows No Borders
Fuad Aleskerov, Tenured Professor and Director of the International Centre of Decision Choice and Analysis at HSE University, together with his colleagues, has developed methods of network analysis in bibliometrics that have made it possible to identify patterns in the appearance and citation of publications in academic journals, as well as their influence on each other. When one or a number of studies are frequently cited by a wide range of journals, this is an indicator that the research is of high quality. By contrast, extensive cross-citation within a limited group of journals increases the likelihood of identifying a network of predatory publications.

 

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