?
Применение алгебры подстановок для унификации программ
Труды Института системного программирования РАН. 2011. Т. 21. С. 141-166.
Захаров В. А., Новикова Т. А.
Для решения многих задач системного программирования, к числу которых относятся задачи реорганизации программ, деобфускации программ, выявления уязвимостей в программном коде и др., желательно иметь инструментальное средство, позволяющее обнаруживать фрагменты программ, имеющие сходное поведение. Современные средства обнаружения программных клонов позволяют выявлять лишь фрагменты программ, имеющие сходное синтаксическое устройство, поскольку более глубокий семантический анализ программ сталкивается с алгоритмической неразрешимостью проблемы функциональной эквивалентности программ. Для того чтобы избежать алгоритмически трудных задач проверки функциональной эквивалентности, авторы настоящей статьи предлагают воспользоваться более сильным разрешимым отношением эквивалентности программ – логико-термальной эквивалентностью, – введенной в 1972 г. В.Э. Иткиным. В данной статье разработан новый алгоритм проверки логико-термальной эквивалентности программ, основанный на операции вычисления точной нижней грани в решетке конечных подстановок. На основе этого алгоритма авторам статьи удалось также решить задачу логико-термальной унификации программ, которая состоит в построении для двух заданных фрагментов программного кода такой процедуры, которая представляет собой наиболее общую специализацию этих двух фрагментов.
Научное направление:
Компьютерные науки
Приоритетные направления:
компьютерно-математическое
Язык:
русский
Захаров В. А., Новикова Т. А., Труды Института системного программирования РАН 2012 Т. 23 С. 455-476
Унифицировать два алгебраических выражения и означает отыскать такую подстановку термов вместо переменных этих выражений, чтобы оба терма и имели одинаковое значение. Задачу унификации можно распространить и на программы. Унифицировать две программы и означает отыскать такие цепочки присваиваний и ...
Добавлено: 30 сентября 2015 г.
Захаров В. А., Новикова Т. А., Труды Института системного программирования РАН 2014 Т. 26 № 2 С. 245-268
Задача унификации пары подстановок θ_1 и θ_2 состоит в вычислении такой пары подстановок η' и η'', чтобы композиции θ_1 η' и θ_2 η'' были равны. По существу, задача унификации подстановок равносильна задаче решения линейных уравнений вида θ_1 X=θ_2 Y в полугруппе подстановок. Но некоторые линейные уравнения над подстановками также можно рассматривать как новые варианты задачи ...
Добавлено: 30 сентября 2015 г.
Захаров В. А., Новикова Т. А., Труды Института системного программирования РАН 2012 Т. 22 С. 435-455
Логико-термальная эквивалентность программ – это одно из наиболее слабых отношений эквивалентности программ, аппроксимирующих отношение функциональной эквивалентности и обладающих разрешающим алгоритмом. В данной статье предложена новая модификация алгоритма проверки логико-термальной эквивалентности программ, основанная на операции вычисления точной нижней грани в решетке конечных подстановок. Показано, что трудоемкость предложенного алгоритма оценивается величиной O(n6) , где n - размер ...
Добавлено: 30 сентября 2015 г.
Викентьева О. Л., Полякова О. А., Пермь : Издательство Пермского национального исследовательского политехнического университета, 2019
В учебном пособии рассмотрены вопросы применения основных принципов структурного программирования в сложных программных системах на языке высокого уровня С++, которые демонстрируются на содержательных примерах. ...
Добавлено: 16 сентября 2020 г.
Захаров В. А., Кузюрин Н. Н., Варновский Н. П. и др., Программирование 2015 № 6
Обфускацией программ называется такое эквивалентное преобразование программ, которое придает программе форму, затрудняющую понимание алгоритмов и структур данных, используемых программой, и препятствующую извлечению из текста программы определенной полезной информации, содержащейся в ней. Поскольку обфускация программ может найти широкое применение при решении многих задач криптографии и компьютерной безопасности, задаче оценки стойкости обфускации придается очень большое значение, начиная ...
Добавлено: 13 октября 2015 г.
Захаров В. А., Cybernetics and Systems Analysis 2010 № 4 С. 39-48
В статье показано, каким образом двухленточные автоматы можно применять для проверки эквивалентности последовательных программ. Семантика последовательных программ определяется на основе моделей динамической логики. В том случае, когда динамическая шкала ациклична (т.е. в программе нет взаимно обратимых операторов), она может быть описана двухленточным детерминированным автоматом. Тогда задача проверки эквивалентности программ, семантика операторов которых определяется динамическими ...
Добавлено: 30 сентября 2015 г.
Chernyshev S. V., Cherepanov E. A., Pankratiev E. V. и др., Journal of Mathematical Sciences 2005 Vol. 128 No. 6 P. 3487-3495
Добавлено: 27 января 2014 г.
Skoptsov K. A., Sheshenin S., Галатенко В. В. и др., International Journal of Applied Mechanics 2016 Vol. 8 No. 2 P. 1650016-01-1650016-18
We present a method for evaluating elastic properties of a composite material produced by molding a resin filled with short elastic fibers. A flow of the filled resin is simulated numerically using a mesh-free method. After that, assuming that spatial distribution and orientation of fibers are not significantly changed during polymerization, effective elastic moduli of ...
Добавлено: 22 мая 2016 г.
Малышев Д. С., Discrete Mathematics 2015 Vol. 338 No. 11 P. 1860-1865
We completely determine the complexity status of the 3-colorability problem for hereditary graph classes defined by two forbidden induced subgraphs with at most five vertices. © 2015 Elsevier B.V. All rights reserved. ...
Добавлено: 7 апреля 2014 г.
Springer, 2012
Добавлено: 29 января 2013 г.
Сотникова С. Ю., Динамика сложных систем 2012 № 3 С. 84-87
В статье описывается разработанный программный комплекс моделирования физических процессов, который также позволяет проводить идентификацию параметров печатного узла (физической модели), на котором реализуется проектируемый бортовой источник вторичного электропитания. Для него разработаны интерфейсы связи управляющей программы с известными программами моделирования и оптимизации. ...
Добавлено: 5 декабря 2014 г.
Chuprikov P., Николенко С. И., Davydow A. и др., IEEE Transactions on Networking 2018 Vol. 26 No. 1 P. 342-355
Добавлено: 14 марта 2018 г.
Карпов В. Э., Карпова И. П., Procedia Engineering 2015 Vol. 100 P. 1459-1468
Добавлено: 14 марта 2015 г.
М. : Издательский центр «Российский государственный гуманитарный университет», 2019
Сборник включает 27 докладов международной конференции по компьютерной лингвистике и интеллектуальным технологиям «Диалог 2019», не вошедшие в ежегодник «Компьютерная лингвистика и интеллектуальные технологии», но рекомендованные Программным Комитетом к представлению на конференции. Для специалистов в области теоретической и прикладной лингвистики и интеллектуальных технологий. ...
Добавлено: 10 декабря 2019 г.
Беклемишев Л. Д., Оноприенко А. А., Математический сборник 2015 Т. 206 № 9 С. 3-20
Формулируются системы преобразований термов, число шагов работы которых на произвольном входе конечно, но не ограничивается никакой вычислимой функцией, доказуемо тотальной в арифметике Пеано PА. Тем самым, утверждение о сходимости таких систем не доказуемо в PA. Эти системы получаются из независимого комбинаторного утверждения, известного как принцип червя; их также можно рассматривать как вариант хорошо известной игры Геракла и гидры, ...
Добавлено: 13 марта 2016 г.
Bliznets Ivan, Cygan M., Komosa P. и др., ACM Transactions on Computation Theory 2018 Vol. 10 No. 2 P. 1-32
Добавлено: 30 октября 2018 г.
Добавлено: 15 декабря 2015 г.
Шуранов Е. В., / Cornell University. Series Computer Science "arxiv.org". 2021.
Добавлено: 14 февраля 2023 г.
Гостев И. М., М. : Юрайт, 2016
В настоящее время компьютерные науки стремительно развиваются. Новые версии операционных систем появляются каждые полтора-два года, поэтому было принято решение о включении в данную книгу такого материала, который не будет устаревать. Содержание учебника представляет собой некоторые наиболее общие принципы построения операционных систем, которые были разработаны более 50 лет назад и практически не изменились за прошедшее время. ...
Добавлено: 13 октября 2009 г.
Borchmann D., Hanika T., Объедков С. А., Discrete Applied Mathematics 2020 Vol. 273 P. 30-42
Добавлено: 29 октября 2019 г.
Каз. : Издательство «Фэн» Академии наук Республики Татарстан, 2013
Материалы и доклады Шестой Всероссийской научно-практической конференции по имитацонному моделированию и его применению в науке и промышленности. ...
Добавлено: 14 декабря 2013 г.
В статье представлена технология, позволяющая собирать в полевых исследованиях пространственно локализованные данные об объектах городской среды. Технология основана на автоматической привязке фотографий к пространственным координатам. Приведен план полевых и камеральных мероприятий, предложены варианты ГИС-обработки собираемых таким образом данных. В качестве примера приведены данные об использовании белорусского языка в общественном пространстве городов Белоруссии. ...
Добавлено: 12 апреля 2015 г.
Байбикова Т. Н., Доморацкий Е. П., Вестник Московского финансово-юридического университета 2017 № 1 С. 200-206
В статье рассмотрены вопросы визуализации научной информации, особенности применения когнитивной компьютерной графики, выделен круг задач научной визуализации. Приведены краткий обзор, тенденции развития и основные характеристики современных средств программной визуализации. Разработан модуль визуализации для системы численного анализа геометрических характеристик изображений объектов. ...
Добавлено: 10 июня 2017 г.