Исследование и развитие алгоритмов верификации программных моделей недетерминированных вычислительных систем, оперирующих строковыми данными

Множество строк символов представляет собой фундаментальный тип данных для большинства вычислительных систем и используется в большинстве языков программирования. Ошибки в программах, преобразующих строки, являются одной из основных причин уязвимости безопасностипередачи информации.Предполагаемое исследование ставит перед собой цель: изучение и развитие алгоритмов верификации программных моделей недетерминированных вычислительных систем с бесконечным числом cостояний, которые оперируют строковыми данными.Программные модели вычислительных систем можно пытаться автоматически верифицировать посредством инструментов анализа и преобразования программ, изначально разработанных для решения других задач, - подходящим образом ставя им задачу на преобразование и пытаясь преобразовать скрытые в контексте задачи верификации семантические свойства программной модели на явный синтаксический уровень. Т.е. в синтаксические термины, в которых проверяемыесвойствамоделибудут очевидны.Для этих целей, в рамках предполагаемого проекта, предполагается исследовать и развивать возможности автоматических оптимизаторов программ, написанных на (функциональных) языках высокого уровня. Более конкретно: предполагается развивать алгоритмы семантических методов преобразования программ, основанные на широко применяемом подходе развертки/свертки (unfold-fold) дерева возможных вычислений анализируемой gрограммы. Автоматическая специализация программ по контексту их применения является одним из таких методов оптимизации программ.