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

SMT solvers are widely used instruments as math core for symbolic executions and theorem proving in both software and hardware. Defects (bugs) presence in SMT solvers implementation determines not only their quality but also correctness of the tools using SMT solvers for their purposes. This work suggests a solution for SMT solvers testing as a way of automatic defect detection based on behaviour difference of SMT solvers in form of SMT formulas coverage difference. The core of a suggested solution is a combination of searching behaviour difference of a testing system, model counting problem (#SAT, #SMT), and black-box fuzzing. Let an SMT formula coverage be a variables states set in condition of presence such variables in the formula while the formula satisfiability preserving, then two formulas coverage difference will be a marker of defects presence in one of the solvers. The program module of SMT solvers defects detection has been implemented based on this way. The obtained results show the possibility of using the technology for automatic defects detection in SMT solvers.

• 1. Существующие подходы обнаружения дефектов в SMT-решателях
  • 1.1. Фаззинг-тестирование
    • 1.1.1. Фаззинг-тестирование, основанное на грамматике
    • 1.1.2. Фаззинг-тестирование, основанное на случайных неэквивалентных мутациях
    • 1.1.3. Фаззинг-тестирование, основанное на эквивалентных мутациях
  • 1.2. Резюме
• 2. Постановка задачи
  • 2.1. Основные функции разрабатываемого подхода
  • 2.2. Требования к сбору покрытия
    • 2.2.1. Атом как предмет покрытия
  • 2.3. Требования к отчету о покрытии
  • 2.4. Дефекты в SMT-решателях
  • 2.5. Резюме
• 3. Подход к автоматическому обнаружению дефектов в SMT-решателях
  • 3.1. Описание подхода обнаружения дефектов
    • 3.1.1. Алгоритм подхода обнаружения дефектов
    • 3.1.2. Оптимизация на основе множественного выбора атомов
  • 3.2. Получение атомов из формулы
  • 3.3. Инкрементальность решений
  • 3.4. Резюме
• 4. Разработка модуля обнаружения дефектов
  • 4.1. API доступа к SMT-решателям
    • 4.1.1. JavaSMT
    • 4.1.2. PySMT
    • 4.1.3. ScalaSMT
    • 4.1.4. KSMT
    • 4.1.5. Резюме
  • 4.2. Входные данные
  • 4.3. Архитектура модуля
  • 4.4. Подготовка исходной формулы
  • 4.5. Сбор покрытия
  • 4.6. Сравнение покрытия
  • 4.7. Резюме
• 5. Тестирование
  • 5.1. Описание тестовой выборки
  • 5.2. Задача тестирования
  • 5.3. Ход тестирования
  • 5.4. Результаты тестирования
  • 5.5. Анализ результатов
  • 5.6. Проблемы
  • 5.7. Резюме
• 1. Листинги
• 2. фрагмент бенчмарка