?
Automated Formal Verification of Model Transformations Using the Invariants Mechanism
P. 59–73.
The article is devoted to the problem of automated formal verification of modeling artifacts during engineering of digital transformations. Automation significantly increases the quality of model transformations since many manual errors are eliminated. However, the formal checking the correctness of such automation remains an open question. One more problem is the dependence of the procedure for checking the correctness of transformations on the modeling languages of the source and target models. In the article we represent the solution, based on the formalism of invariant checking, that allows modelers to formally test the correctness of model transformation regardless of a modeling language.
In book
Issue 365: Perspectives in Business Informatics Research. , Switzerland: Springer, 2019.
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
Maria V. Demina, Anna R. Ishchenko, Journal of Geometry and Physics 2025 Vol. 216 Article 105596
We develop a method based on the Darboux theory of integrability that is able to produce first integrals of geodesic equations on 2-surfaces. We present local explicit examples of two-dimensional metrics with polynomial in momenta first integrals of arbitrary degrees. We also find metrics admitting transcendental first integrals. In particular, we express some first integrals ...
Added: November 19, 2025
Maria V. Demina, Varvara G. Nechitailo, Qualitative Theory of Dynamical Systems 2025 Vol. 24 No. 1 Article 29
We classify generalized Liénard differential equations, sometimes called Liénard type equations, that have integrating factors of a special form. We present first integrals of the related equations. Our families of equations contain almost all known integrable generalized Liénard equations as partial cases. We find the necessary and sufficient conditions of the Liouvillian integrability for the ...
Added: April 7, 2025
С. М. Авдошин, А. М. Литвиненко, Информационные технологии 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 ...
Added: January 23, 2025
Проскуряков К. А., Lyadova L. N., В кн.: Технологии разработки инструментальных средств (ТРИС-2024) : Материалы XIV Международной научно-технической конференции.: Таганрог: Издательство ЮФУ, 2024. С. 207–219.
Abstract: The goal of the project is to approve an approach to generating code implementing user data visualization models based on metamodels of visual domain-specific languages (DSL), created to describe visualization models, and descriptions of formal grammars of target textual programming languages presented in a multi-aspect ontology. The ontology also includes descriptions of “Model-Text” transformation ...
Added: December 11, 2024
A. D. Dzheiranian, Ermakov I. D., Proskuryakov K. A. et al., Scientific Vizualisation 2024 Vol. 16 No. 4 P. 82–101
An approach to the development of data visualization tools is described that provides the ability to customize to the needs of users and the specifics of the domains in which they work, based on domain-specific modeling. The results of the analysis of data visualization tools and the possibility of customizing them to subject area based ...
Added: November 24, 2024
Джейранян А. Д., Ермаков И. Д., Проскуряков К. А. et al., В кн.: GraphiCon 2024: Материалы 34-й Международной конференции по компьютерной графике и машинному зрению (Россия, Омск, 17–19 сент. 2024 г.).: Омск: Издательство ОмГТУ, 2024. С. 300–314.
An approach to the development of data visualization tools is described that provides the ability to customize to the needs of users and the specifics of the domains in which they work, based on domain-specific modeling. The results of the analysis of data visualization tools and the possibility of customizing them to subject area based ...
Added: November 15, 2024
A. D. Dzheiranian, Ermakov I. D., Proskuryakov K. A. et al., Proceedings of the Institute for System Programming of the RAS 2024 Vol. 36 No. 2 P. 127–140
The data visualization method based on a language-oriented approach is proposed. An analysis of data visualization tools and their customizability for subject areas based on user needs has been carried out. It is noted that these tools require highly qualified users to customize the data visualization format (users must have programming skills). It is proposed ...
Added: July 29, 2024
Ulitin, B., Babkin, E., Babkina, T., , in: Model-Driven Organizational and Business Agility: Second International Workshop, MOBA 2022, Leuven, Belgium, June 6–7, 2022, Revised Selected PapersIssue 457: Model-Driven Organizational and Business Agility. MOBA 2022.: Switzerland: Springer, 2022. P. 110–124.
The use of intelligent systems with advanced AI algorithms is a key aspect of enterprise digitalization. The railway domain is not an exception. We argue, that the quality of any AI-based system greatly depends on the methods of computer-human interaction. We propose an approach to organize the interaction of the end user with the AI-based ...
Added: October 25, 2022
Gnatenko A., Zakharov V., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 776–785
Sequential reactive systems include programs and devices that work with two streams of
data and convert input streams of data into output streams. Such information processing systems
include controllers, device drivers, computer interpreters. The results of operation of such computing
systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite
transducers are most often ...
Added: January 17, 2022
Vinarskii E., Zakharov V., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 751–762
Sequential reactive systems include hardware devices and software programs which operate
in continuous interaction with the external environment, from which they receive streams of input signals
(data, commands) and in response to them form streams of output signals. Systems of this type
include controllers, network switches, program interpreters, system drivers. The behavior of some
reactive systems is determined not ...
Added: January 17, 2022
Gnatenko A., Zakharov V., Моделирование и анализ информационных систем 2021 Т. 28 № 4 С. 356–371
Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification ...
Added: January 17, 2022
Ulitin B., Babkina T. S., , in: Lecture Notes in Business Information ProcessingIssue 423: Advanced Information Systems Engineering Workshops. CAiSE 2021.: Switzerland: Springer, 2021. P. 81–92.
The process of implementing agile technologies in an enterprise is an example of a highly demanding and challenging topic both for practitioners and academy. Speaking about agility, we basically mean various kinds of automation. A higher degree of automation results in a more agile enterprise. However, in practice, even in the case of complete automation ...
Added: June 9, 2021
Korotyaev Evgeny, Saburova N., Mathematische Annalen 2020 Vol. 337 P. 723–758
We consider a Laplacian on periodic discrete graphs. Its spectrum consists of a finite
number of bands. In a class of periodic 1-forms, i.e., functions defined on edges of
the periodic graph, we introduce a subclass of minimal forms with a minimal number
I of edges in their supports on the period. We obtain a specific decomposition of ...
Added: February 5, 2021
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
Boris Ulitin, Eduard Babkin, , in: Lecture Notes in Information Systems and OrganisationIssue 40: Digital Transformation and New Challenges. Digitalization of Society, Economics, Management and Education.: Switzerland: Springer, 2020. P. 37–48.
The research is related to the problem of coherent evolution of a domain-specific language (DSL) in response to evolution of the application domain and users’ capabilities. We offer a solution of that problem based on a particular model-driven approach. We give the whole definition of DSL in terms of model-oriented approach. Such definition allows us ...
Added: June 10, 2020
Gnatenko A., Zakharov V., Automatic Control and Computer Sciences, Allerton Press Inc., United States 2019 Vol. 53 No. 7 P. 663–675
One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a nite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. A behaviour of such a reactive system displays itself in the correspondence between ows of control signals ...
Added: October 17, 2019
Zakharov V., Винарский Е. М., В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019).: М.: Изд-во механико-математического факультета МГУ, 2019. С. 257–260.
Конечные автоматы Мили, представляющие собой простейшую математическую модель преобразования потоковых данных, широко используются во многих областях информатики. Но для некоторых приложений большое значение имеют не только значения обрабатываемых данных и порядок их следования, но также интервалы времени, которые отделяют события, присходящие по ходу вычисления автомата. Такие свойства уже не описывается явно средствами классической теории конечных ...
Added: October 17, 2019
Gnatenko A., Zakharov V., В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019).: М.: Изд-во механико-математического факультета МГУ, 2019. С. 263–266.
Описаны синтаксис и семантика нового расширения Reg-CTL* темпоральной логики деревьев вычислений CTL*, предназначенного для спецификации и верификации вычислений последовательных реагирующих систем. Поеказано, что задача верификации моделей автоматов-преобразователей относительно выполнимости формул логики CTL* является PSPACE-полной. ...
Added: October 17, 2019
Cham: Springer, 2015.
This book constitutes the refereed proceedings of the 10th International Andrei Ershov Informatics Conference, PSI 2015, held in Kazan and Innopolis, Russia, in August 2015.
The 2 invited and 23 full papers presented in this volume were carefully reviewed and selected from 56 submissions. The papers cover various topics related to the foundations of program and ...
Added: January 29, 2019
Springer, 2018.
This book constitutes the refereed proceedings of the 4th International Conference on Tools and Methods for Program Analysis, TMPA 2017, Moscow, Russia, March 3-4, 2017.
The 12 revised full papers and 5 revised short papers presented together with three abstracts of keynote talks were carefully reviewed and selected from 51 submissions. The papers deal with topics such as ...
Added: November 12, 2018
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