• 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
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.
September 21, 2026
Researchers Develop Methodology to Assess the Quality of Legal Representation in Criminal Proceedings
Having a good defence attorney in criminal proceedings can largely determine whether a defendant retains their freedom, health and good name. Researchers at HSE University propose a method for predicting an attorney’s performance based on the outcomes of their previous cases. The methodology takes into account the severity of the charges, the complexity of the cases, and the most likely outcome, drawing on judicial statistics.
September 21, 2026
Algebra, Geometry, and AI: Russian and Vietnamese Mathematicians Discuss Current Research
A delegation of scientists from Hanoi visited the HSE Faculty of Computer Science and then took part in a Russian-Vietnamese conference in St Petersburg. The events were part of the three-year project ‘Flexibility and Computational Methods.’ Over the course of the project, the researchers have prepared joint publications and obtained new mathematical results.

 

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