Аннотация. 
Задача разработки SAT-решателя для поиска верификационных наборов в тестировании программного обеспечения

Данная работа посвящена автоматической генерации верификационных наборов тестовых процедур; предложен и разработан алгоритм нахождения тестовых наборов посредством трансляции программ в логические формулы и их преобразования для решения задачи выполнимости булевых формул.

Ключевые слова: тестовые наборы, автоматическая генерация, решатель, булевы ограничения.

Актуальность разработки систем автоматизированного тестирования (SAT)

Верификация программного обеспечения (ПО) является наиболее важным и в то же время трудоемким этапом разработки систем с высокой ценой ошибки. Любое несоответствие таких систем выдвинутым к ним требованиям может привести к большим финансовым потерям, гибели людей и ущербу окружающей среде. Методы верификации ПО активно развиваются с середины XX века и с каждым годом возрастает потребность в их автоматизации. Тестирование является наиболее распространенным и универсальными способом поиска ошибок в программах, но сталкивается с множеством трудностей при увеличении сложности систем.

Существует множество методов обнаружения ошибок и контроля качества программ, совокупность которых называется верификацией программного обеспечения. Сейчас активно развиваются системы, предполагающие автоматическое доказательство соответствия ПО так называемой спецификации, т. е. предъявляемым к нему требованиям. Тем не менее, в большинстве крупных проектов в основе процесса верификации до сих пор стоит именно тестирование. Зачастую этим занимаются люди, задачей которых является разработка тестов для поиска ошибок, допущенных в коде программистами. Обычно тесты представляют собой набор «входных» параметров, подающихся на вход в программу, а по завершении ее работы «выходные» параметры сравниваются с «ожидаемыми» по логике, описанной в спецификации.

В работе показано, что задача тестирования ПО может сводиться к задаче выполнимости булевых формул (SAT) и выполнимости формул в теориях (SMT). Существует очевидная возможность перевода простейшего алгоритма в булеву формулу, для которой будут введены некоторые преобразования, позволяющие существенно ограничить полный перебор возможных комбинаций входных параметров.