Table | Card | RUSMARC | |
Allowed Actions: –
Action 'Read' will be available if you login or access site from another network
Action 'Download' will be available if you login or access site from another network
Group: Anonymous Network: Internet |
Annotation
Такие инструменты, как 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.
Document access rights
Network | User group | Action | ||||
---|---|---|---|---|---|---|
ILC SPbPU Local Network | All |
![]() ![]() ![]() |
||||
Internet | Authorized users SPbPU |
![]() ![]() ![]() |
||||
![]() |
Internet | Anonymous |
Table of Contents
- 1. Существующие подходы обнаружения дефектов в SMT-решателях
- 1.1. Фаззинг-тестирование
- 1.1.1. Фаззинг-тестирование, основанное на грамматике
- 1.1.2. Фаззинг-тестирование, основанное на случайных неэквивалентных мутациях
- 1.1.3. Фаззинг-тестирование, основанное на эквивалентных мутациях
- 1.2. Резюме
- 1.1. Фаззинг-тестирование
- 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. Резюме
- 3.1. Описание подхода обнаружения дефектов
- 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. Резюме
- 4.1. API доступа к SMT-решателям
- 5. Тестирование
- 5.1. Описание тестовой выборки
- 5.2. Задача тестирования
- 5.3. Ход тестирования
- 5.4. Результаты тестирования
- 5.5. Анализ результатов
- 5.6. Проблемы
- 5.7. Резюме
- 1. Листинги
- 2. фрагмент бенчмарка
Usage statistics
|
Access count: 0
Last 30 days: 0 Detailed usage statistics |