• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • Логика Хоара для императивного языка, учитывающего некоторые аппаратные ограничения
  • 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
October 1, 2026
HSE Researchers Show How Congenital Motor Disorders Affect Brain Development
Researchers from HSE University’s Institute for Cognitive Neuroscience have synthesised the findings of their previous studies on brain development in children with obstetric brachial plexus palsy and arthrogryposis. Their analysis shows that impaired motor function in early childhood not only limits children’s motor experience but also affects memory, categorical thinking, and information processing. The study has been published in Frontiers in Psychology.
October 1, 2026
Window into the Body: Scientists Develop Neural Network to Detect Risk of 15 Diseases from Retinal Images
Russian universities, with the participation of HSE University, Sber, and Z-union, have developed a neural network that can simultaneously assess the risk of 15 types of pathology from retinal photographs, including not only eye diseases but also cardiovascular conditions. The AI system can help clinicians detect potentially concerning changes at an early stage, identify signs reflecting the condition of retinal blood vessels, and determine whether a patient may need further examination. The paper has been published in Frontiers in Medicine.
September 30, 2026
'We Did Not Limit the Time for Questions'
The International Laboratory for Supercomputer Atomistic Modelling and Multi-Scale Analysis at HSE University held a major conference on molecular dynamics. Participants had the opportunity to attend all the presentations, while speakers were given as much time as they needed to answer questions. The HSE News Service interviewed Grigory Smirnov, Head of the Laboratory, and Genri Norman, Chief Research Fellow, about the conference preparations and the discussions it generated.

 

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

?

Логика Хоара для императивного языка, учитывающего некоторые аппаратные ограничения

С. 74–78.
Ковалев Д. Ю.
Language: Russian
Text on another site
Keywords: формальные методылогика Хоарааксиоматическая семантика

In book

Алгебра, теория чисел, дискретная геометрия и многомасштабное моделирование: современные проблемы, приложения и проблемы истории Материалы XXIII Международной конференции, посвящённой 80-летию профессора Александра Ивановича Галочкина и 75-летию профессора Владимира Григорьевича Чирского
Тула: Тульский государственный педагогический университет им. Л.Н. Толстого, 2024.
Similar publications
Логика Хоара для императивного языка, учитывающего некоторые аппаратные ограничения
Ковалев Д. Ю., Чебышевский сборник 2025 Т. 26 № 3 С. 113–124
In this paper, an imperative programming language considering some hardware limitations of a computer based on the RV32I instruction set is defined, including its syntax and semantics in a form of Hoare logic. The need for such language comes from the fact that formal proofs conducted for programs in languages not considering hardware limitations cannot ...
Added: November 5, 2025
Обзор применения формальных методов в робототехнике
Мордвинов Д. А., Литвинов Ю. В., Научно-технические ведомости Санкт-Петербургского государственного политехнического университета. Информатика. Телекоммуникации. Управление 2016 № 1 (236) С. 84–107
This paper is a survey of applying formal methods in the robotics field. We consider a number of recent works on robotic behavior specification in terms of temporal logics and using the model checking approach. Formal analysis techniques for Petri nets and robotics systems modeling using those methods are also considered. Verification of hybrid systems, ...
Added: October 30, 2018
Анализ непротиворечивости моделей архитектуры предприятия с использованием формальных методов верификации
Babkin E., Пономарев Н. О., Бизнес-информатика 2017 Т. 43 № 3 С. 30–40
Enterprise architecture design is a complex process which makes it possible to synchronize the capabilities and needs of business and information technologies (IT). It can be achieved by clarifying the understanding and formalization of the business processes and the interaction of the elements of the system through their formal description. The large number of interacting ...
Added: October 3, 2018
Proceedings of Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006. ISoLA 2006.
Margaria T., Steffen B., IEEE Computer Society, 2006.
This volume contains the Post-Conference Proceedings of ISoLA 2006, the 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2006), which was held in Paphos, Cyprus on 15th-19th November 2006, sponsored by EASST and in cooperation with the IEEE Technical Committee on Complex Systems. ...
Added: September 30, 2015
Метод определения противоречий в DEMO-моделях бизнес-процессов
Babkin E., Buzueva A., Logvinova K. V., Бизнес-информатика 2014 № 2 С. 33–43
The article analyzes the methods and provides a solution to the problem of detecting logical contradictions in business process models of the health care company. Practical purpose of solving the problem is to increase the efficiency of data management for municipal agencies as stakeholder of company. The methodology is based on formal tools relational logic ...
Added: April 17, 2014
Современные формализованные реконструкции Онтологического аргумента (на примере подхода Э. Залты и П. Оппенгеймера)
Pashchenko T., В кн.: Трансцендентное в современной философии: направления и методы.: СПб.: Алетейя, 2013.
E. Zalta and P. Oppenheimer have created non-modal reading of the Anselm’s argument about the existence of God, The Ontological Argument. The authors have deduced the existence of God from his being. For this purpose, the term "that than which none greater can be conceived" used as a definite description. Through the predicate logic with ...
Added: February 18, 2014
Elections àla russe: formal establishment of rules and informal methods
Gelman V. Y., Osteuropa Zeitschrift für Gegenwartsfragen des Ostens 2005 Vol. 55 No. 10 P. 85–97
Added: November 24, 2013
  • 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