• 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
October 12, 2026
Road Injuries Leading Cause of Death Among Men Aged 10 to 39
Worldwide, road injuries are the leading cause of death among males aged 10–39. An international team of researchers reached this conclusion as part of the Global Burden of Disease Study 2023, analysing data from 204 countries between 1990 and 2023. Their findings have been published in The Lancet Public Health, with HSE University Professor Vasily Vlassov listed among the collaborators.
October 8, 2026
HSE Experts Take Part in 23rd Annual Meeting of Valdai Discussion Club
The 23rd Annual Meeting of the Valdai Discussion Club was held from September 28 to October 1, 2026 under the theme ‘Responsibility for the Future: Limits of the Possible, or Limitless Possibilities?’ The forum brought together 120 experts from 40 countries, including representatives of China, the United States, India, Brazil, the United Kingdom, Germany, Egypt, Iran, and Japan.
October 7, 2026
‘Our Team Consists of True Leaders in Their Respective Academic Disciplines
The HSE International Centre of Decision Choice and Analysis studies a wide range of methods for analysing decision-making and possible scenarios for the development of natural, socio-economic, and political phenomena using various mathematical models. The application of advanced mathematical methods to forecasting helps to prevent negative outcomes and avoid erroneous decisions. The HSE News Service spoke to the centre’s director, Prof. Fuad Aleskerov, about its work.

 

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

?

Обзор методов верификации смарт-контрактов

Информационные технологии. 2025. Т. 31. № 1. С. 42–55.
С. М. Авдошин, А. М. Литвиненко

Smart contracts are software algorithms that represent an agreement in digital form with a mechanism for forcing the parties to fulfill their obligations. Smart contracts are already firmly entrenched in the fields of finance, but this is not the only possible field of application. The disadvantage of such a digital agreement is that smart contracts can contain errors that can lead to financial losses. The verification process is designed to reduce such errors. This paper provides an overview of methods and tools in the field of smart contract verification.

Research target: Computer Science
Language: Russian
Full text
DOI
Text on another site
Keywords: smart contractformal verificationEthereumEthereumформальная верификациятехнология распределенного реестраdistributed ledger technologyvulnerabilities detectionсмарт-контрактпоиск уязвимостей
Similar publications
No Species Is an Island, Entire of Itself: Genetic Speciation Algorithm with Interplay among Species
International Journal of Engineering, Transactions B: Applications 2027 Vol. 40 No. 5 P. 1437–1460
This paper, with a particular emphasis on Genetic Algorithm (GA), proposes a novel approach that integrates clustering mechanisms, predator-prey dynamics, and a distinctive selection strategy for generating subsequent populations. The proposed evolutionary algorithm, referred to as Genetic Speciation Algorithm with Interplay Among Species (GSAIS), is comprehensively evaluated against several variants of GAs as well as ...
Added: October 12, 2026
JavaCapsule: Итеративная генерация и отладка Java-кода на основе структурированной обратной связи
Alexandrov D., Vasilevsky V., Rezunik L. et al., Труды Института системного программирования РАН 2026 Т. 38 № 5 С. 73–90
Large language models demonstrate limitations in tasks that require precise information retrieval from very long input sequences. This limitation affects code generation in large object-oriented systems, where correctness depends on complex inter-class dependencies and the analysis of long execution traces that exceed standard context window sizes. This paper presents JavaCapsule, a technology for automated generation ...
Added: October 12, 2026
Proceedings of the 34th IUPAP Conference on Computational Physics: CCP2023, August 4-8, Kobe, Japan
Singapore: Springer Singapore, 2026.
This volume presents the Proceedings of the 34th IUPAP Conference on Computational Physics (CCP2023), held in Kobe, Japan on August 4–8, 2023. It offers a collection of peer-reviewed articles that highlight recent developments in computational and simulation research across various areas of physics. Key topics include the use of data science, quantum computing, and machine ...
Added: October 12, 2026
РАЗРАБОТКА МЕТОДА И АЛГОРИТМОВ АДАПТИВНОГО ФЕДЕРАТИВНОГО ОБУЧЕНИЯ С УЧЕТОМ РАСПРЕДЕЛЕННОГО ЗАПАЗДЫВАНИЯ КЛИЕНТСКИХ ОБНОВЛЕНИЙ
Zykov S. V., Ермаков С. Р., Современные наукоемкие технологии 2026 № 9 С. 43–53
При федеративном обучении с неоднородными клиентскими данными и переменными задержками запоздавшие обновления могут ухудшать качество модели, а обмен параметрами с глобальным сервером увеличивает сетевую нагрузку. Целью исследования является разработка и теоретико-экспериментальное обоснование метода и алгоритмов адаптивного федеративного обучения с учетом распределенного запаздывания клиентских обновлений. Для обоснования разрабатываемых решений использованы событийная и непрерывная модели градиентных обновлений, ...
Added: October 11, 2026
О воспроизводимости анализа временных рядов на основе матричных профилей
Брычков М. Е., Незнанов А.А., Программирование 2026 № 4 С. 50–66
The matrix profile (MP) quickly became one of the most important time series preprocessing methods when it was introduced in 2016, facilitating the solution of a wide range of time series analysis problems, in particular anomaly and pattern detection problems. The high significance has led to the emergence of various tools for MP calculating, but ...
Added: October 9, 2026
Человеко-машинная система анализа и улучшения качества условий проживания населения
Aleskerov F. T., Вайншток А. П., Делахова А. М. et al., Информационные процессы 2026 Т. 26 № 3 С. 895–913
The development and effective management of territorial entities are priority issues for all states, particularly in the context of the digital transformation of public administration. Over the past decade, the integration of information technologies into municipal and regional planning has significantly altered approaches to strategic development, service delivery, and public engagement. This paper describes the ...
Added: October 9, 2026
Effects of Elevation Changes and Multilevel Structures on Vehicular Signal Propagation
Stepanyants V., Andrey V. Fizulin, Chibirov A. et al., FUTURE TRANSPORTATION 2026 Vol. 6 No. 5 Article 225
Reliable Vehicle-to-Everything (V2X) evaluation requires propagation models that represent terrain and multilevel infrastructure. Most integrated vehicular simulators still rely on planar models, but the magnitude of the resulting bias is unclear. This study quantitatively compares flattened two-dimensional (2D) and terrain-aware three-dimensional (3D) variants of three scenarios using identical Sionna RT settings. The pipeline combines OpenStreetMap ...
Added: October 8, 2026
Автоматизированное построение математических теорий
Люксембург А. А., УРСС, 2005.
Изучается возможность автоматизированного построения математических теорий. Рассматривается дедуктивная система, основанная на языке логики предикатов первого порядка, объектами системы являются математические выражения или формулы, которые описывают математические объекты или их свойства. В дедуктивной системе выводятся математические определения и теоремы. Для доказательства теорем используются методы автоматического доказательства. Разработан алгоритм, выводящий часть формул системы. Для решения задачи используется аппарат математической ...
Added: October 7, 2026
Automated Ranking of Soybean Plots from Close-Range RGB Video via Depth Filtering and Point-Based Counting
Groshev Maksim, Rybakov Petr, Teterin N. et al., Sensors 2026 Article 6171
Manual assessment of soybean yield components, such as pod number, is laborious, time-consuming, and subjective. Existing computer-vision approaches based on object detection or instance segmentation perform poorly on close-range RGB imagery of soybean canopies due to severe occlusions, ambiguous plant boundaries, and the high cost of bounding-box annotation. To address these challenges, we propose a ...
Added: October 7, 2026
«Цифровые» акционерные общества: правовой статус корпорации
Иванова Е. Е., Право. Журнал Высшей школы экономики 2026 № 3 С. 109–137
The article is devoted to analyzing the legal status of digital joint-stock companies (DJSCs) and their participants under Russian law, in the context of the question of singling out DJSCs as an independent legal form of a legal entity. Drawing on the first DJSCs registered in Russia, it examines the procedure for their incorporation, the ...
Added: October 7, 2026
Decision support system for improving the quality of life of the population
Aleskerov F. T., Chaika E., Дерендяев А. Б. et al., Procedia Computer Science 2026 No. 287 P. 590–595
Under conditions of dynamic socio-economic changes, effective planning and decision-making are key factors in ensuring a high quality of life for the population in territories. This paper presents a decision support system for territorial administrations for the development and implementation of sustainable development strategies, using one of the regions of the Russian Federation – the ...
Added: October 7, 2026
Новые информационные технологии в исследовании сложных структур. Материалы шестнадцатой международной конференции 21–25 Сентября 2026 г.
Томск: Издательство Томского государственного университета, 2026.
Материалы сборника Шестнадцатой Международной конференции «Новые информационные технологии в исследовании сложных структур» (Москва, 21–25 сентября 2026 г.) ориентированы на широкий круг специалистов, работающих на стыке теории информации, системного анализа и прикладных предметных областей. В издание вошли результаты исследований, посвящённые моделированию дискретных и стохастических структур управления и связи, разработке высокопроизводительных вычислительных и телекоммуникационных систем, а также вопросам цифровой трансформации образования, архитектурно-градостроительного проектирования,  экологического ...
Added: October 6, 2026
Оптимизация энергопотребления предприятия с использованием методов многокритериальной оптимизации
Серебренников Д. А., Belov A. V., Информационные технологии и вычислительные системы 2026 № 3 С. 157–169
В условиях роста стоимости энергоресурсов и необходимости повышения энергоэффективности производственных процессов особую актуальность приобретает задача оптимизации энергопотребления промышленных предприятий. В данной работе рассматривается подход к управлению энергозатратами машиностроительного предприятия на основе методов многокритериальной оптимизации. Постановка задачи включает несколько целевых функций: минимизацию энергопотребления, минимизацию стоимости электроэнергии с учётом тарифных ограничений и максимизацию производственной эффективности. Для решения ...
Added: October 5, 2026
On Practical Aspects of Constructing Quasi-Cyclic Subfield Subcodes of Dual Elliptic Codes and Their Application in McEliece-type Cryptosystems
Kuninets A., IEEE Transactions on Information Theory 2026 P. 1–1
In this work we study the applicability of Quasi-Cyclic Subfield Subcodes of Dual Elliptic (QC-SSDE) codes for integration into code-based cryptographic schemes. Detailed algorithms are provided for constructing parity-check matrices as well as block-circulant parity-check matrices for this family of codes, accompanied by empirical results that enable the construction of QC-SSDE codes with predetermined dimensions. ...
Added: October 3, 2026
Инкрементальный метод обновления многомерного куба по неупорядоченному потоку событий журналов информационных систем
Zykov S. V., Уфимцев Г. А., Моделирование, оптимизация и информационные технологии 2026 Т. 14 № 8 С. 1–13
Информационные системы формируют большие объёмы событийных журналов, которые используются для анализа работы приложений и сервисов. При этом события могут поступать в аналитический контур позже момента их фактического возникновения и не в исходном порядке. Такая рассинхронизация приводит к ошибкам при построении агрегированных временных показателей, а регулярный полный пересчёт многомерного аналитического куба требует значительных вычислительных затрат. Целью ...
Added: October 2, 2026
Polarization of opinions in the group: a modeling algorithm considering the dynamics of social bonds
Chebotarev V., Andreyuk D., Elizarova Anastasiya et al., Procedia Computer Science 2022 Vol. 213 No. C P. 596–601
The dynamics of opinion in a group are of interest for a number of practical purposes. In particular, consensus helps and polarization of opinions hinders cohesive teamwork. Existing approaches for modeling opinion dynamics mostly do not take into account the dynamism of social relations in a group. This paper proposes an algorithm and a program ...
Added: October 2, 2026
Enhancing Boundary Stability in Decision Trees and Random Forests: A Weighted Sample Duplication Approach
Konstantinov A., Elizarova Anastasiya P., Utkin L., Computing, Telecommunications and Control 2026 Vol. 19 No. 1 P. 16–25
Decision trees and their ensemble extensions, such as random forests, are widely used as classification models due to their simplicity and interpretability. However, in many real-world tasks where class labels overlap in the feature space, standard decision trees rely on hard splits that create fragile decision boundaries. In these regions, small perturbations in the input ...
Added: October 2, 2026
Bayesian Adaptive Sparse Copula
Prokhorov A., Burda M., Journal of Computational and Graphical Statistics 2026 P. 1–13
Bayesian nonparametric density estimation procedures are typically based on single-scale priors, such as Dirichlet process mixtures. Alternative multiscale density priors built on decision trees have many well-known advantages, including the ability to characterize abrupt local changes and to provide an estimate with a desired level of resolution. Despite their theoretical appeal, multiscale methods have typically ...
Added: October 2, 2026
Pericyte-derived cancer-associated fibroblasts correlate with poor survival and are enriched after chemoradiotherapy in glioblastoma
Aly Ismailov, Poptsova M., Plos One 2026 Vol. 21 No. 9 Article e0355902
Added: October 2, 2026
ПЕРСПЕКТИВЫ ИСПОЛЬЗОВАНИЯ ЦИФРОВОГО РУБЛЯ БИЗНЕСОМ
Баширов М. Ф., Кулешова Е. П., Бизнес. Общество. Власть 2025 № 1 (55) С. 119–127
The article analyzes the key aspects of the digital ruble, outlined in the official concept published by the Bank of Russia. The possible advantages for business, the state and society noted in the document are considered, and a number of recommendations are proposed that will allow realizing all the positive aspects of the new monetary ...
Added: August 10, 2026
Synthetic Proofs with Tool-Integrated Reasoning: Contrastive Alignment for LLM Mathematics with Lean
Obozov M., Diskin M., Beznosikov A. et al., , in: Proceedings of The 3rd Workshop on Mathematical Natural Language Processing (MathNLP 2025).: Suzhou: Association for Computational Linguistics, 2025. Ch. 15 P. 195–202.
Modern mathematical reasoning benchmarks primarily focus on answer finding rather than proof verification, creating a gap in evaluating the proving capabilities of large language models (LLMs). We present a methodology for generating diverse mathematical proof tasks using formal tools. Our approach combines Lean-based synthetic problem generation with a Tool-Integrated Reasoning (TiR) framework for partial (sampling-based) ...
Added: February 26, 2026
Нормы Гражданского кодекса Российской Федерации и цифровые технологии: вопросы судебной практики
Volos A., Lex Russica (Русский закон) 2025 Т. 78 № 5 С. 68–76
Автор формирует научно обоснованные выводы о направлениях развития судебной практики по вопросам применения недавно появившихся в ГК РФ норм, связанных с использованием цифровых технологий субъектами экономического оборота. В статье делается принципиальное заключение о том, что суды нередко используют рассматриваемые нормы не в том контексте, который имелся в виду при их создании. Практика по данным делам ...
Added: May 18, 2025
Can Ethereum predict Bitcoin’s volatility?
Teterin M., Peresetsky A., Applied Econometrics 2025 Vol. 77 P. 74–90
Bitcoin and Ethereum are the two world’s largest cryptocurrencies. Their market capitalizations have recently peaked, making them more attractive to portfolio investors. As the cryptocurrency market is known for its high volatility nature, government institutions are also interested in this segment of the financial market for more comprehensive regulation. Volatility forecasting is a crucial part ...
Added: April 22, 2025
О роли типовых контрактов в стандартизации государственных закупок
Lyutova O. I., Байрашев В. Р., Вопросы государственного и муниципального управления 2025 № 1 С. 116–141
В статье рассматриваются проблемы применения типовых контрактов в контексте происходящей цифровизации государственных закупок, осуществляемой путем перехода к цифровым (машиночитаемым) государственным контрактам. Выдвигаются гипотезы о признании процесса разработки типовых контрактов без учета мнения заинтересованных сторон в качестве значимого препятствия при подготовке государственного контракта, а также о возможности сокращения затрат на подготовку закупок за счет наделения типовых ...
Added: March 28, 2025
  • 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