• 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

?

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

Моделирование и анализ информационных систем. 2012. Т. 19. № 6. С. 45–56.
Волканов Д. Ю., Zakharov V., Зорин Д. А., Коннов И. В., Подымов В. В.
Priority areas: IT and mathematics mathematics
Language: Russian
Keywords: верификациясистемы реального времени
Similar publications
Three Algorithms for Merging Hierarchical Navigable Small World Graphs
Ponomarenko A., / Series Computer Science "arxiv.org". 2025.
This paper addresses the challenge of merging hierarchical navigable small world (HNSW) graphs, a critical operation for distributed systems, incremental indexing, and database compaction. We propose three algorithms for this task: Naive Graph Merge (NGM), Intra Graph Traversal Merge (IGTM), and Cross Graph Traversal Merge (CGTM). These algorithms differ in their approach to vertex selection ...
Added: July 30, 2026
Профессиональная верификация: Руководство по продвинутой функциональной верификации
Уилкокс П., Romanov A., М.: ДМК Пресс, 2025.
Книга, которую вы держите в руках, продолжает серию «Книжная полка истового инженера», которая издается при поддержке компании YADRO. Данная книга представляет собой учебник по теоретическим основам продвинутой функциональной верификации и содержит лучшие практики, используемые в настоящее время. В ней подробно описана унифицированная методология верификации (UVM) и раскрыты такие темы, как функциональный виртуальный прототип, функциональное покрытие, утверждения, формальная верификация, тестбенчи, косимуляция, эмуляция, аппаратное ...
Added: July 30, 2026
New bound on S1× S2-setting Bell locality of a nonseparable Werner state
Loubenets E. R., / Series arxiv.org "quant-ph". 2026. No. 2607.18050.
In many quantum applications it is important to know whether or not a Bell nonlocal two-qudit state exhibits its nonlocality under correlation scenarios with some given numbers S1,S2≥1 of generalized quantum measurements at two sites. In the present article, we find analytically a new general locality condition sufficient for a  nonseparable Werner state with a ...
Added: July 21, 2026
On functional equations for Chow polylogarithms
Bolbachan V., / Series math "arxiv.org". 2024.
Chow polylogarithms are some special functions arising in explicit description of the Beilinson regulator map. The most interesting functional equation for this function reflects its vanishing on the boundary in the Bloch's cycle complex. We show that this functional equation formally follows from more simple ones, namely skew-symmetry, functoriality and multiplicativity. To prove this, we study ...
Added: July 16, 2026
On Goncharov’s conjecture in next to Milnor degree
Bolbachan V., / Series math "arxiv.org". 2024.
Let K be a field of characteristic zero. We prove that its motivic cohomology in degree m−1 and weight m is rationally isomorphic to the cohomology of the polylogarithmic complex. This gives a partial extension of A. Suslin theorem describing the indecomposable K3 of a field. ...
Added: July 16, 2026
Statistical inference based on band-limited kernels: Rational-infinitely divisible distributions and beyond
Panov V., Ryabchenko A., / Series arXiv "stat.ME". 2026. No. 2607.05048.
This paper investigates the problem of statistical inference for a mixture distribution consisting of a discrete and a continuous component, with a particular focus on the class of rational-infinitely divisible distributions. We consider non-parametric estimation of both components of the mixture as well as the quasi-L{é}vy measure, assuming that the mixture belongs to the class ...
Added: July 9, 2026
Growth in noncommutative algebras and entropy in derived categories
Piontkovski D., / Series arXiv "math". 2026.
A noncommutative projective variety is defined, following Artin and Zhang, by a graded coherent algebra 𝐴. The category of coherent sheaves is then the quotient qgr(𝐴) of the category of finitely presented graded modules by the subcategory of torsion modules. We consider the categorical and polynomial entropies of the Serre twist, that is, of the ...
Added: June 23, 2026
Multilinear nilalgebras and the Jacobian theorem
Piontkovski D., / Series arXiv "math". 2025.
If a symmetric multilinear algebra is weakly nil, then it is Engel. This result may be regarded as an infinite-dimensional analogue of the well-known Jacobian theorem, which states that if a polynomial mapping has a polynomial inverse, then its Jacobian matrix is invertible. This refines a theorem of Gerstenhaber and partially answers a question posed ...
Added: June 23, 2026
Strong Approximations for Markov Chains Weakly Converging to Diffusions
Konakov V., Kucher D., Mammen E., / Series arXiv "math". 2026. No. 2606.11142v1.
In this paper, we construct strong approximations for discrete-time Markov chains weakly converging to continuous diffusion processes, as well as for their perturbed counterparts. Under the assumption of bounded coefficients, we construct closely coupled versions of these processes on a shared probability space. In particular, for both non-degenerate and degenerate cases, we maximize the probability ...
Added: June 11, 2026
ML-based Fast Simulation of FARICH Responses
Shipilov F., Barnyakov A., Ivanov A. et al., / Series Physics "arxiv.org". 2026.
A fast simulation of the detector response is a vital task in high-energy physics (HEP). Traditional Monte-Carlo methods form the backbone of modern particle physics simulation software but are computationally expensive. We present a machine-learning-based approach to fast simulation of the Focusing Aerogel Ring Imaging Cherenkov (FARICH) detector response. Given a particle track and momentum, ...
Added: May 19, 2026
Bifurcations and Structural Stability of Generic PC-HC Families
Dorovskiy A., / Series arXiv "math". 2026.
In this paper the structural stability of generic families of vector fields of the PC-HC class on the two-dimensional sphere is proved. A classification of these families up to moderate equivalence in neighborhoods of their large bifurcation supports is presented, based on such invariants as the configuration and the characteristic set. The realization lemma is proved. ...
Added: May 14, 2026
On the minimum number of maximal distance-k independent sets in trees
Taletskii D., / Series arXiv "math". 2026.
A vertex subset of a graph is called a \textit{distance-$k$ independent set} if the distance between any two of its distinct vertices is at least $k + 1$. For all $n,k \geq 1$, we determine the minimum possible number of inclusion-wise maximal distance-$k$ independent sets among all $n$-vertex trees. It equals~$n$ if $n \leq k ...
Added: May 1, 2026
On Arithmetic Mirror Symmetry for smooth Fano fourfolds
Ovcharenko M., / Series arXiv "math". 2026.
We introduce an explicit class of tempered Laurent polynomials in the sense of Villegas and Doran--Kerr in n⩽4 variables including all Landau--Ginzburg models for smooth Fano threefolds with very ample anticanonical class. We check that it contains Landau--Ginzburg models for various Fano fourfolds which are complete intersections in smooth toric varieties and Grassmannians of planes, ...
Added: April 30, 2026
Natural hazard database from Internet publications: text mining with a large language model
Derkacheva A., Sakirkina M., Kraev G. et al., /. 2026.
Comprehensive data on natural hazards and their consequences are crucial for effective for risk assessment, adaptation planning, and emergency response. However, many countries face challenges with fragmented, inconsistent, and inaccessible data, particularly regarding local-scale events. To address this data gap in Russia, we developed an end-to-end processing pipeline that scrapes news from various online sources, ...
Added: April 28, 2026
Имитационное моделирование. Теория и практика (ИММОД 2025)
СПб.: АО "ЦТСС", 2025.
В научном издании представлены труды Двенадцатой всероссийской научно-практической конференции по имитационному моделированию и его применению в науке и промышленности «Имитационное моделирование. Теория и практика» (ИММОД-2025) по следующим направлениям: - теоретические основы и методология имитационного и комплексного моделирования; - методы исследования и оценки качества моделей, валидация и верификации моделей; - методы и системы распределенного моделирования; - ...
Added: April 17, 2026
Evaluation of Correlation Functions and Multi-model Forecasting of Geopotential Height and Temperature in the Troposphere and Lower Stratosphere
Gordin V. A., Smirnov M. A., Russian Meteorology and Hydrology 2025 No. 50 P. 1016–1028
Statistical evaluation of three-dimensional auto- and cross-correlation functions for increments from the first guess was performed to interpolate the complex forecast (postprocessing) of geopotential height and temperature to regular grid points. The forecast fields from the ICON model were used as the first guess. Positive definiteness was provided in the evaluation. The verification of the ...
Added: February 17, 2026
InGrid: Towards a Simulation-Based Automated Decision-Making System for Transportation
Stepanyants V., , in: 2025 International Russian Automation Conference (RusAutoCon).: IEEE, 2025. P. 982–986.
Transportation systems are complicated and deal with significant problems. With the pool of possible solutions being wide, extensive transportation planning has to be involved. However, planning based on expert opinions is significantly limited in terms of rapidity, accuracy, and confidence. Computer-aided design and automated decision-making systems are the next step to ensure transportation system development ...
Added: October 3, 2025
Wind Speed Analysis Method within WRF-ARW Tropical Cyclone Modeling
Poplavsky E., Kuznetsova A., Troitskaya Y., Journal of Marine Science and Engineering 2023 Vol. 11 No. 6 Article 1239
This paper presents an analysis of a new method for retrieving the parameters of the atmospheric boundary layer in hurricanes. This method is based on the approximation of the upper parabolic part of the wind speed profile and the retrieval of the lower logarithmic part. Based on the logarithmic part, the friction velocity, near-surface wind ...
Added: December 10, 2024
О проблеме доказательств в историческом исследовании, или Подозревал ли Петр I патриарха Адриана в связях с мятежными стрельцами?
Akelev E., ВИВЛIОθИКА: E-Journal of Eighteenth-Century Russian Studies 2023 Т. 11 С. 241–270
Как практикующие историки приходят к тем или иным убеждениям? Как отличить «гипотетическое» от «доказанного»? Почему в определенный момент те или иные интерпретации находят всеобщую поддержку в научном сообществе, а другие нет? И как в дальнейшем общепризнанные интерпретации могут быть опровергнуты? Эти вопросы находятся в центре внимания этой статьи, но рассматриваются не отвлеченно, на уровне теории, ...
Added: November 23, 2023
Автоматическая верификация многосторонних соглашений и планирование отправки сообщений в системах распределенного реестра
Федотов И. А., Хританков А. С., Обидаре М. Д., Программная инженерия 2022 № 4 С. 200–208
Многосторонние соглашения используются в системах распределенного реестра и блокчейн-сетях для согласования изменений в системе. Если один из участников сети предлагает транзакцию на запись, то сначала ее должны подтвердить определенные участники сети. Многостороннее соглашение, или консенсус, определяет состав этих участников. На основе предыдущих ответов можно посчитать вероятность подтверждения транзакции для каждого из участников. В настоящей работе ...
Added: September 20, 2022
InnoChain: распределенный реестр для индустриального применения с формальной верификацией на всех уровнях реализации
Кухаренко В. А., Зиборов К. В., Садыков Р. Ф. et al., Моделирование и анализ информационных систем 2020 Т. 27 № 4 С. 454–471
Степень применения методов формальной верификации в индустриальных проектах всегда была ограничена. Распространение систем распределенного реестра (СРР), известных также как блокчейн, быстро меняет ситуацию. Поскольку основной областью применения СРР является автоматизация финансовых транзакций, свойства предсказуемости и надежности являются критическими при реализации таких систем. Реальное поведение СРР определяется выбранным протоколом консенсуса, свойства которого нуждаются в строгой спецификации ...
Added: May 31, 2021
Using an extension of CTL* for specification and verification of sequential reactive systems
Gnatenko A., Zakharov V., Системная информатика 2020 Vol. 17 P. 21–32
Sequential reactive systems such as controllers, device drivers, computer interpreters operate with two data streams and transform input streams of data (control signals, instructions) into output streams of control signals (instructions, data). Finite state transducers are widely used as an adequate formal model for information processing systems of this kind. Since runs of transducers develop ...
Added: November 9, 2020
Научный подход и универсальная этика
Storchevoy M., В кн.: Мораль и универсальностьВып. 3.: М.: Издательский дом "Гуманитарий", 2020. С. 147–160.
В этой статье мы обосновываем тезис о том, что универсальная этика может быть построена на основе научного подхода, что позволяет обосновать ее универсальность и спасти от методологических обвинений в субъективизме или релятивизме. Вначале мы объясняем выбор критериев научности: 1) точная терминология, 2) корректный логический анализ, 3) эмпирическая верификация, 4) точность эмпирических измерений. Затем мы выстраиваем ...
Added: October 31, 2020
«Пороги» между доходными группами: результаты анализа рисков бедности
Slobodenyuk E., В кн.: Модель доходной стратификации российского общества: динамика, факторы, межстрановые сравнения.: Издательство Нестор-История, 2018. Гл. 1.4 С. 93–116.
The chapter covers the issue of monetary relative poverty line location in modern Russia. As it follows from international studies on income stratification it should be placed between 0.5 to 0.75 of median per capita income. Based on the poverty risk data, it is shown that the 0.5 line can be applied as a deep poverty line, and the ...
Added: April 16, 2019
  • 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