|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ИНХС РАН |
||
Верифицированная тактика Isabelle/HOL для теории ограниченных целых на основе инстанцирования и SMTстатья
Статья опубликована в журнале из списка RSCI Web of Science
Статья опубликована в журнале из перечня ВАКДата последнего поиска статьи во внешних источниках: 1 февраля 2021 г.
- Авторы: Sadykov Rafael Faritovich, Mandrykin Mikhail Usamovich
- Журнал: Труды Института системного программирования РАН (электронный журнал)
- Том: 32
- Номер: 2
- Год издания: 2020
- Первая страница: 107
- Последняя страница: 124
- Номер статьи: 9
- DOI: 10.15514/ispras-2020-32(2)-9
- Аннотация: При дедуктивной верификации Си-программ как с помощью различных платформ верификации (Why3, Frama-C/WP, F*), так и с помощью систем интерактивного доказательства теорем (Isabelle, HOL4, Coq) достаточно широко используются SMT-решатели. Их разрешающие алгоритмы полны для некоторых комбинаций логических теорий (логик), в частности для логики QF_UFLIA. В то же время при верификации Си-программ часто необходимо оперировать формулами в других разрешимых логиках, поддерживаемых не всеми SMT-решателями. Типичными примерами таких логик могут служить комбинации QF_UFLIA c теориями ограниченных целых как с переполнением (для беззнаковых целых в Си), так и без переполнения (для знаковых целых), а также теорией конечных интерпретируемых множеств (для поддержки рамочных условий) и др. Одним из возможных способов поддержки таких логик является их непосредственная реализация в SMT-решателях, однако этот способ часто является трудоемким, а также недостаточно гибким и универсальным. Другим способом является реализация пользовательских стратегий инстанцирования кванторов для сведения формул в неподдерживаемых логиках к формулам в широко распространенных разрешимых логиках, таких как QF_UFLIA. В данной статье представлена процедура инстанцирования лемм для трансляции формул в теории ограниченных целых без переполнения в логику QF_UFLIA. Для процедуры трансляции даны доказательства корректности и полноты, а также описана формализация этих доказательств в системе Isabelle/HOL. Аналогичный подход можно использовать для формулирования и доказательства полноты процедур трансляции формул в других теориях, таких как теория ограниченных целых с переполнением и теория ограниченной адресной арифметики.
- Добавил в систему: Садыков Рафаэль Фаритович