?
О минимизации схем программ относительно логико-термальной эквивалентности
С. 84-87.
Захаров В. А., Жайлауова Ш. Р.
Эффективная разрешимость проблемы л-т эквивалентности дает возможность приступить к решению задачи минимизации - построения схемы программ наименьшего размера, л-т эквивалентной заданной схеме. Чтобы отыскать ее решение, заметим, что модель вычислений стандартных схем программ сходна модели вычислений автоматов-преобразователей, работающих над полугруппами. Ранее был предложен метод минимизации автоматов-преобра\-зо\-вателей, работающих над упорядоченными левосократимыми полугруппами. В данной заметке мы покажем, что этим методом можно воспользоваться для минимизации стандартных схем программ относительно л-т эквивалентности в случае, когда эти схемы определены над ортогональными консервативными подстановками.
В книге
М. : МГУ, МАКС Пресс, 2017
Захаров В. А., Жайлауова Ш. Р., Моделирование и анализ информационных систем 2017 Т. 24 № 4 С. 415-433
Стандартные схемы программ - это одна из наиболее простых моделей последовательных императивных программ, предназначенная для решения задач оптимизации и верификации программ. Мы рассматриваем разрешимое отношение логико-термальной эквивалентности стандартных схем программ и задачу минимизации их размера при условии сохранением отношения логико-термальной эквивалентности. Нами доказано, что эта задача является алгоритмически разрешимой. Далее показано, что стандартные схемы программ ...
Добавлено: 12 октября 2017 г.
Захаров В. А., Новикова Т. А., Труды Института системного программирования РАН 2014 Т. 26 № 2 С. 245-268
Задача унификации пары подстановок θ_1 и θ_2 состоит в вычислении такой пары подстановок η' и η'', чтобы композиции θ_1 η' и θ_2 η'' были равны. По существу, задача унификации подстановок равносильна задаче решения линейных уравнений вида θ_1 X=θ_2 Y в полугруппе подстановок. Но некоторые линейные уравнения над подстановками также можно рассматривать как новые варианты задачи ...
Добавлено: 30 сентября 2015 г.
Захаров В. А., Новикова Т. А., В кн. : Дискретные модели в теории управляющих систем : IX Международная конференция, Москва и Подмосковье, 20-22 мая 2015 г.: Труды. : М. : МАКС Пресс, 2015. С. 173-176.
В статье предложена новая модель последовательных императивных программ, использующих средства работы с динамической памятью (указателями, списками и пр.) ...
Добавлено: 12 октября 2015 г.
Захаров В. А., Попеско У. В., В кн. : Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.). : М. : Изд-во механико-математического факультета МГУ, 2016. С. 196-198.
Стандартные схемы программ были введены для разработки математических методов решения задач трансляции, оптимизации и верификации последовательных операторных программ. Ранее было показано, что логико-термальная эквивалентность аппроксимирует функциональную эквивалентность стандартных схем программ. Другое достоинство логико-термальной эквивалентности состоит в том. что это отношение разрешимо за полиномиальное время. Возникает вопрос: можно уточнить отношение логико-термальной эквивалентности, сохранив при этом ее полиномиальную ...
Добавлено: 13 октября 2016 г.
Захаров В. А., Cybernetics and Systems Analysis 2010 № 4 С. 39-48
В статье показано, каким образом двухленточные автоматы можно применять для проверки эквивалентности последовательных программ. Семантика последовательных программ определяется на основе моделей динамической логики. В том случае, когда динамическая шкала ациклична (т.е. в программе нет взаимно обратимых операторов), она может быть описана двухленточным детерминированным автоматом. Тогда задача проверки эквивалентности программ, семантика операторов которых определяется динамическими ...
Добавлено: 30 сентября 2015 г.
Захаров В. А., Гнатенко А. Р., В кн. : Проблемы теоретической кибернетики: XVIII международная конференция (Пенза, 19-23 июня 2017 г.). : М. : МГУ, МАКС Пресс, 2017. С. 68-71.
В статье в качестве формальной модели последовательных реагирующих систем была предложена модель вычислений конечных автоматов-преобразователей, работающих над полугруппами действий. Для спецификации поведений таких автоматов был предложен специальный вариант темпоральной логики линейного времени LTL-FL (LTL with Formal Languages). Формальные языки (множества конечных слов фиксированных алфавитов) в формулах LTL-FL используются для параметризации темпоральных операторов. В этой же ...
Добавлено: 22 октября 2017 г.
Захаров В. А., Новикова Т. А., Труды Института системного программирования РАН 2012 Т. 23 С. 455-476
Унифицировать два алгебраических выражения и означает отыскать такую подстановку термов вместо переменных этих выражений, чтобы оба терма и имели одинаковое значение. Задачу унификации можно распространить и на программы. Унифицировать две программы и означает отыскать такие цепочки присваиваний и ...
Добавлено: 30 сентября 2015 г.
Захаров В. А., Новикова Т. А., Труды Института системного программирования РАН 2012 Т. 22 С. 435-455
Логико-термальная эквивалентность программ – это одно из наиболее слабых отношений эквивалентности программ, аппроксимирующих отношение функциональной эквивалентности и обладающих разрешающим алгоритмом. В данной статье предложена новая модификация алгоритма проверки логико-термальной эквивалентности программ, основанная на операции вычисления точной нижней грани в решетке конечных подстановок. Показано, что трудоемкость предложенного алгоритма оценивается величиной O(n6) , где n - размер ...
Добавлено: 30 сентября 2015 г.
Миронкин В. О., Обозрение прикладной и промышленной математики 2018 Т. 25 № 1 С. 3-8
Исследованы граф внутренних состояний Sponge-конструкции и взаимосвязь между внутренними состояниями и элементами выходной последовательности. Предложены методы построения коллизий, использующие особенности цикловой структуры подстановки Sponge-конструкции. Описан общий вид соответствующих коллизий. ...
Добавлено: 27 апреля 2018 г.
Захаров В. А., Temerbekova G., Automatic Control and Computer Sciences 2017 Vol. 51 No. 7 P. 523-530
Добавлено: 13 октября 2016 г.
Захаров В. А., Новикова Т. А., Труды Института системного программирования РАН 2011 Т. 21 С. 141-166
Для решения многих задач системного программирования, к числу которых относятся задачи реорганизации программ, деобфускации программ, выявления уязвимостей в программном коде и др., желательно иметь инструментальное средство, позволяющее обнаруживать фрагменты программ, имеющие сходное поведение. Современные средства обнаружения программных клонов позволяют выявлять лишь фрагменты программ, имеющие сходное синтаксическое устройство, поскольку более глубокий семантический анализ программ сталкивается с ...
Добавлено: 30 сентября 2015 г.
Захаров В. А., Jaylauova S., Automatic Control and Computer Sciences 2017 Vol. 51 No. 7 P. 689-700
Добавлено: 19 декабря 2017 г.
Захаров В. А., Темербекова Г. Г., Моделирование и анализ информационных систем 2016 Т. 23 № 6 С. 741-753
Автоматы-преобразователи над полугруппами можно использовать в качестве модели последовательных реагирующих программ, работающих в постоянном взаимодействии со своим окружением. Получив очередную порцию данных, реагирующая программа выполняет некоторую последовательность действий и предъявляет результат. Такие программы возникают при проектировании компьютерных драйверов, алгоритмов, работающих в оперативном режиме, сетевых коммутаторов. Во многих случаях проблема верификации программ такого рода может быть ...
Добавлено: 13 октября 2016 г.
М. : МГУ, МАКС Пресс, 2017
Книга представляет собой сборник статей, написанных на основе докладов, представленных на 18-ой Международной конференции "Теоретические проблемы кибернетики" в Пензенском государственном университете, 19-23 июня 2017 г. ...
Добавлено: 12 октября 2017 г.
Захаров В. А., Temerbekova G., Системная информатика 2016 No. 7 P. 33-44
Добавлено: 13 октября 2016 г.
Подымов В. В., Захаров В. А., Труды Института системного программирования РАН 2014 Т. 26 № 3 С. 145-166
В статье исследована задача проверки эквивалентности последовательных программ, некоторые операторы которых обладают свойствами перестановочности и подавления. Два оператора считаются перестановочными, если результат их последовательного выполнения не зависит от порядка, в котором эти операторы выполняются. Считается, что оператор b подавляет оператор a, если последовательное выполнение операторов a и b дает такой же результат, что и выполнение ...
Добавлено: 29 сентября 2015 г.
Соснин А. В., Балакина Ю. В., Кащихин А. Н., Вестник Санкт-Петербургского университета. Язык и литература 2022 Т. 19 № 1 С. 125-148
Статья посвящена оценке качества перевода: рассматриваются прикладные и прагматические аспекты оценки качества перевода в условиях стремительного увеличения
числа текстов, которые требуется перевести для обеспечения межкультурной коммуникации; суммируется большое количество подходов, каждый из которых при оценке
качества перевода имеет свои преимущества и недостатки; анализируется соотношение категорий адекватности и эквивалентности перевода как основных параметров
оценки. Заключается, что эквивалентность ориентирована на ...
Добавлено: 31 мая 2022 г.
Медведева Е. А., Ряпин И. Ю., Урванцев И. В. и др., Thermal Engineering (English translation of Teploenergetika) 2016 Vol. 63 No. 9 P. 611-620
This paper analyzes the cost-effectiveness of the use of renewable energy sources (RES) and peat in production of electric and heat energy in rural places of the country by comparing tariffs (prices) of energy versus total expenditures on generation of electric and heat energy when using RES and peat. The appraisal of a cost-effective scale ...
Добавлено: 9 октября 2016 г.
Vladislav Podymov, Fundamenta Informaticae 2016 Vol. 147 No. 2-3 P. 315-336
Добавлено: 9 октября 2016 г.
Подымов В. В., Вестник Московского университета. Серия 15: Вычислительная математика и кибернетика 2012 № 4 С. 37-43
В работе предложен метод решения проблемы эквивалентности линейных унарных рекурсивных программ. Основная его идея состоит в сведении проблемы эквивалентности к известным задачам на графах и задачам теории групп. Выделен класс программных семантик, для которых проблема эквивалентности рассматриваемых программ разрешима за полиномиальное время с использованием предложенной методики. ...
Добавлено: 29 сентября 2015 г.
Авраамова О. Д., Фомин Д. Б., Серов В. А. и др., Математические вопросы криптографии 2021 Vol. 12 No. 2 P. 21-38
Рассматриваются способы реализации нелинейного преобразования блочного алгоритма шифрования с длиной блока 128 бит «Кузнечик» (ГОСТ Р 34.12-2015) и хеш-функции «Стрибог» (ГОСТ Р 34.11-2012). Показана возможность реализации подстановки за 226 логических операций. ...
Добавлено: 26 июля 2021 г.
Фомин Д. Б., Прикладная дискретная математика. Приложение 2021 № 14 С. 51-55
Рассмотрены способы построения дифференциально 2δ-равномерных подстано- вок на F_{2^{2m}} для случая m≥3. Предложенный подход излагается с использованием так называемого TU-представления функций и обобщает известный способ построения дифференциально 4-равномерных подстановок поля F_{2^{2m}} с применением подстановки обращения ненулевых элементов поля. ...
Добавлено: 22 сентября 2021 г.
Захаров В. А., В кн. : Материалы XVII международной конференции "Проблемы теоретической кибернетики". : Каз. : Отечество, 2014. С. 100-102.
Показано, что задача проверки k-значности конечного автомата-преобразователя, работающего над полугруппой, вложимой в разрешимую группу, может быть решена за время, полиномиальное относительно размера автомата. ...
Добавлено: 13 октября 2015 г.
Высоцкий Л. И., Жуков В. В., Шуплецов М. С., В кн. : Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС-2018). Вып. 1.: М. : ИППМ РАН, 2018. С. 30-37.
При обнаружении ошибок или изменении
спецификации
проектируемой
сверхбольшой
интегральной схемы (СБИС) на поздних этапах
маршрута проектирования откат на более ранние этапы
проектирования и их повторное выполнение очень часто
становится непрактичным в силу существенных
временных затрат. Для целей сокращения времени
проектирования
в
современные
маршруты
проектирования интегрируют специальные этапы
функциональной коррекции схемы (англ. Engineering
Change Order, ECO). В основе указанного подхода лежит
анализ уже спроектированной схемы и построение
небольшой подсхемы-заплатки, внедрение которой в уже
синтезированную ...
Добавлено: 10 ноября 2020 г.