?
Verification, Model Checking, and Abstract Interpretation. 18th International Conference, VMCAI 2017, Paris, France, January 15–17, 2017, Proceedings
Хам :
Springer, 2016.
Bouajjani A., Monniaux D.
This book constitutes the refereed proceedings of the 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017, held in Paris, France, in January 2017. The 27 full papers together with 3 invited keynotes presented were carefully reviewed and selected from 60 submissions. VMCAI provides topics including: program verification, model checking, abstract interpretation and abstract domains, program synthesis, static analysis, type systems, deductive methods, program certification, debugging techniques, program transformation, optimization, hybrid and cyber-physical systems.
Язык:
английский
Гнатенко А. Р., Захаров В. А., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 776–785
Добавлено: 17 января 2022 г.
Гнатенко А. Р., Захаров В. А., Моделирование и анализ информационных систем 2021 Т. 28 № 4 С. 356–371
К последовательным реагирующим системам относятся компьютерные программы и вычислительные устройства, которые обрабатывают потоки входных данных или сигналов управления и генерируют на выходе последовательности команд или результатов вычислений. Для проектирования таких систем полезно иметь формальные языки спецификаций, способные выражать отношения между входными и выходными потоками данных. В предшествующих работах нами было предложено семейство таких языков спецификаций, ...
Добавлено: 17 января 2022 г.
Vadim Azhmyakov, Oxford: Elsevier, 2019.
Добавлено: 30 октября 2021 г.
Гнатенко А. Р., Захаров В. А., Системная информатика 2020 Vol. 17 P. 21–32
Последовательные реагирующие системы, такие как контроллеры, системные драйверы, компьютерные интерпретаторы, работают с двумя потоками данных и преобразуют входные потоки данных (управляющие сигналы, инструкции) в выходные потоки управляющих сигналов (инструкции, данные). Конечные преобразователи широко используются в качестве подходящей формальной модели для подобных систем обработки информации. Поскольку вычисления преобразователей протекают во времени, темпоральная логика, очевидно, может использоваться ...
Добавлено: 9 ноября 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 г.
Boris Ulitin, Eduard Babkin, Tatiana Babkina и др., , in: Lecture Notes in Business Information ProcessingIssue 365: Perspectives in Business Informatics Research.: Switzerland: Springer, 2019. P. 59–73.
Добавлено: 30 сентября 2019 г.
Камкин А. С., М.: МАКС Пресс, 2018.
Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М.В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации ...
Добавлено: 2 ноября 2018 г.
Захаров В. А., Гнатенко А. Р., , in: Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018.: Yaroslavl: Ярославский государственный университет им. П.Г. Демидова, 2018. P. 29–36.
Добавлено: 26 октября 2018 г.
Гнатенко А. Р., Захаров В. А., Моделирование и анализ информационных систем 2018 Т. 25 № 5 С. 506–524
О выразительных возможностях некоторых расширений линейной темпоральной логики // Моделирование и анализ информационных систем. — 2018. — Т. 25, № 5. — С. 506–524. Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых ...
Добавлено: 26 октября 2018 г.
Кулямин В. В., Lavrischeva E. M., Mutilin V. S. и др., Proceedings of the Institute for System Programming of the RAS 2016 Vol. 28 No. 3 P. 189–208
This paper regards problems of analysis and verification of complex modern operating systems, which should take into account variability and configurability of those systems. The main problems of current interest are related with conditional compilation as variability mechanism widely used in system software domain. It makes impossible fruitful analysis of separate pieces of code combined ...
Добавлено: 11 августа 2018 г.
Гнатенко А. Р., Захаров В. А., Proceedings of the Institute for System Programming of the RAS 2018 Vol. 30 No. 3 P. 303–324
Добавлено: 14 июня 2018 г.
Гнатенко А. Р., Захаров В. А., В кн.: Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды.: МГУ, МАКС Пресс, 2018. С. 131–133.
Проведено сравнение выразительных возможностей темпоральной логики LP-CTL*. В этой логике были выделены два класса формул (фрагмента) LP-1-LTL и LP-n-LTL и показано, что фрагмент LP-1-LTL превосходит по выразительным возможностям известную темпоральную логику линейного времени LTL, а фрагмент LP-n-LTL имеет такие же выразительные возможности, что и монадическая логика второго порядка с одной функцией следования S1S. ...
Добавлено: 14 июня 2018 г.
Хорошилов А. В., Мандрыкин М. У., , in: Perspectives of System Informatics - 11th International Andrei P. Ershov Informatics Conference, PSI 2017, Moscow, Russia, June 27-29, 2017, Revised Selected Papers, Lecture Notes in Computer ScienceVol. 10742.: Springer, 2018. P. 256–275.
Добавлено: 12 февраля 2018 г.
Бухаров О. Е., Боголюбов Д. П., Приборы и системы. Управление, контроль, диагностика 2018 № 1 С. 25–33
В статье описан процесс разработки гибридной системы поддержки принятия решения для работы с классом слабоструктурированных задач с недоопределенными переменными. Приводится общая постановка задач прогнозирования и оценивания для класса слабоструктурированных задач. Обосновано использование интервальных нейронных сетей и генетических алгоритмов при решении таких задач. Описан разработанный автором алгоритм обучения интервальных нейронных сетей. Рассмотрена схема предлагаемой системы поддержки ...
Добавлено: 9 февраля 2018 г.
Cham: Springer, 2017.
This book constitutes the refereed proceedings of the 13th International Haifa Verification Conference, HVC 2017, held in Haifa, Israel in November 2017. The 13 revised full papers presented together with 4 poster and 5 tool demo papers were carefully reviewed and selected from 45 submissions. They are dedicated to advance the state of the art and state of the ...
Добавлено: 24 января 2018 г.
Захаров В. А., Гнатенко А. Р., В кн.: Проблемы теоретической кибернетики: XVIII международная конференция (Пенза, 19-23 июня 2017 г.).: М.: МГУ, МАКС Пресс, 2017. С. 68–71.
В статье в качестве формальной модели последовательных реагирующих систем была предложена модель вычислений конечных автоматов-преобразователей, работающих над полугруппами действий. Для спецификации поведений таких автоматов был предложен специальный вариант темпоральной логики линейного времени LTL-FL (LTL with Formal Languages). Формальные языки (множества конечных слов фиксированных алфавитов) в формулах LTL-FL используются для параметризации темпоральных операторов. В этой же ...
Добавлено: 22 октября 2017 г.
Switzerland: Springer, 2017.
This book constitutes the proceedings of the 38th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2017, held in Zaragoza, Spain, in June 2017. Petri Nets 2017 is co-located with the Application of Concurrency to System Design Conference, ACSD 2017.
The 16 papers, 9 theory papers, 4 application papers, and 3 tool papers, ...
Добавлено: 6 мая 2017 г.
Захаров В. А., Kozlova D., , in: Proceedings of the 25th International Workshop on Concurrency, Specification and Programming, Rostock, Germany, September 28-30, 2016.Vol. 1698.: Humboldt-Universität zu Berlin, 2016. P. 233–244.
Добавлено: 13 октября 2016 г.
Захаров В. А., Козлова Д. Г., В кн.: Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.).: М.: Изд-во механико-математического факультета МГУ, 2016. С. 204–206.
Характерная особенность моделей Крипке и большинства темпоральных логик (PLTL, CTL, PDL, mu-исчисление и др.), используемых в качестве формальных языков спецификации, состоит в том, что элементарные свойства вычислений зависят только от состояний модели, но не от вычислений, которыми достигаются состояния. Однако для стороннего наблюдателя поведение реагирующей системы проявляется в соответствии между последовательностями стимулов (сигналов), которыми внешняя ...
Добавлено: 13 октября 2016 г.