?
Automated Formal Verification of Model Transformations Using the Invariants Mechanism
P. 59–73.
Язык:
английский
В книге
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., Дискин М. С., Безносиков А. Н. и др., , in: Proceedings of The 3rd Workshop on Mathematical Natural Language Processing (MathNLP 2025).: Suzhou: Association for Computational Linguistics, 2025. Ch. 15 P. 195–202.
Добавлено: 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 ...
Добавлено: 19 ноября 2025 г.
Maria V. Demina, Varvara G. Nechitailo, Qualitative Theory of Dynamical Systems 2025 Vol. 24 No. 1 Article 29
Добавлено: 7 апреля 2025 г.
С. М. Авдошин, А. М. Литвиненко, Информационные технологии 2025 Т. 31 № 1 С. 42–55
Смарт-контракты — программные алгоритмы, которые представляют собой соглашение в цифровой форме
с наличием механизма принуждения сторон к выполнению обязательств. Смарт-контракты уже крепко закрепились в сферах финансов, однако это не единственная возможная сфера применения. Недостаток такого цифрового соглашения заключается в том, что смарт-контракты могут содержать ошибки, потенциально
приводящие к финансовым потерям. Процесс верификации проводится для того, чтобы снизить ...
Добавлено: 23 января 2025 г.
Проскуряков К. А., Лядова Л. Н., В кн.: Технологии разработки инструментальных средств (ТРИС-2024) : Материалы XIV Международной научно-технической конференции.: Таганрог: Издательство ЮФУ, 2024. С. 207–219.
Аннотация: Цель проекта – апробация подхода к генерации кода, реализующего пользовательские модели визуализации данных, на основе метамоделей визуальных предметно-ориентированных языков (DSL), созданных для описания моделей визуализации, и описаний формальных грамматик целевых текстовых языков, представленных в многоаспектной онтологии. Онтология включает также и описания правил трансформации типа «Модель-Текст» (генерации кода). Эти правила могут быть расширены для создания ...
Добавлено: 11 декабря 2024 г.
A. D. Dzheiranian, Ermakov I. D., Proskuryakov K. A. и др., Scientific Vizualisation 2024 Vol. 16 No. 4 P. 82–101
Добавлено: 24 ноября 2024 г.
Джейранян А. Д., Ермаков И. Д., Проскуряков К. А. и др., В кн.: GraphiCon 2024: Материалы 34-й Международной конференции по компьютерной графике и машинному зрению (Россия, Омск, 17–19 сент. 2024 г.).: Омск: Издательство ОмГТУ, 2024. С. 300–314.
Описывается подход к разработке средств визуализации данных, обеспечивающий возможность настройки на потребности пользователей и специфику предметных областей, в которых они работают, основанный на предметно-ориентированном моделировании. Кратко представлены результаты анализа инструментов визуализации данных и возможности их настройки на предметные области исходя из потребностей пользователей и решаемых ими задач. Показано, что существующие инструменты требуют от пользователей навыков ...
Добавлено: 15 ноября 2024 г.
A. D. Dzheiranian, Ermakov I. D., Proskuryakov K. A. и др., Proceedings of the Institute for System Programming of the RAS 2024 Vol. 36 No. 2 P. 127–140
Предлагается метод визуализации данных, основанный на языково-ориентированном подходе. Проведен анализ инструментов визуализации данных и возможности их настройки на предметные области исходя из потребностей пользователей. Отмечено, что эти инструменты требуют от пользователей высокой квалификации для настройки формата визуализации данных (пользователи должны иметь навыки программирования). Предлагается настраивать средства визуализации под нужды пользователей и специфику решаемых пользователями задач ...
Добавлено: 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.
Добавлено: 25 октября 2022 г.
Гнатенко А. Р., Захаров В. А., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 776–785
Добавлено: 17 января 2022 г.
Винарский Е. М., Захаров В. А., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 751–762
Добавлено: 17 января 2022 г.
Гнатенко А. Р., Захаров В. А., Моделирование и анализ информационных систем 2021 Т. 28 № 4 С. 356–371
К последовательным реагирующим системам относятся компьютерные программы и вычислительные устройства, которые обрабатывают потоки входных данных или сигналов управления и генерируют на выходе последовательности команд или результатов вычислений. Для проектирования таких систем полезно иметь формальные языки спецификаций, способные выражать отношения между входными и выходными потоками данных. В предшествующих работах нами было предложено семейство таких языков спецификаций, ...
Добавлено: 17 января 2022 г.
Ulitin B., Бабкина Т. С., , in: Lecture Notes in Business Information ProcessingIssue 423: Advanced Information Systems Engineering Workshops. CAiSE 2021.: Switzerland: Springer, 2021. P. 81–92.
Добавлено: 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 ...
Добавлено: 5 февраля 2021 г.
Гнатенко А. Р., Захаров В. А., Системная информатика 2020 Vol. 17 P. 21–32
Последовательные реагирующие системы, такие как контроллеры, системные драйверы, компьютерные интерпретаторы, работают с двумя потоками данных и преобразуют входные потоки данных (управляющие сигналы, инструкции) в выходные потоки управляющих сигналов (инструкции, данные). Конечные преобразователи широко используются в качестве подходящей формальной модели для подобных систем обработки информации. Поскольку вычисления преобразователей протекают во времени, темпоральная логика, очевидно, может использоваться ...
Добавлено: 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.
Добавлено: 10 июня 2020 г.
Гнатенко А. Р., Захаров В. А., 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 ...
Добавлено: 17 октября 2019 г.
Захаров В. А., Винарский Е. М., В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019).: М.: Изд-во механико-математического факультета МГУ, 2019. С. 257–260.
Конечные автоматы Мили, представляющие собой простейшую математическую модель преобразования потоковых данных, широко используются во многих областях информатики. Но для некоторых приложений большое значение имеют не только значения обрабатываемых данных и порядок их следования, но также интервалы времени, которые отделяют события, присходящие по ходу вычисления автомата. Такие свойства уже не описывается явно средствами классической теории конечных ...
Добавлено: 17 октября 2019 г.
Гнатенко А. Р., Захаров В. А., В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019).: М.: Изд-во механико-математического факультета МГУ, 2019. С. 263–266.
Описаны синтаксис и семантика нового расширения Reg-CTL* темпоральной логики деревьев вычислений CTL*, предназначенного для спецификации и верификации вычислений последовательных реагирующих систем. Поеказано, что задача верификации моделей автоматов-преобразователей относительно выполнимости формул логики CTL* является PSPACE-полной. ...
Добавлено: 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 ...
Добавлено: 29 января 2019 г.
Камкин А. С., М.: МАКС Пресс, 2018.
Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М.В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации ...
Добавлено: 2 ноября 2018 г.