Preview

Труды Института системного программирования РАН

Расширенный поиск

Верифицированная тактика Isabelle/HOL для теории ограниченных целых на основе инстанцирования и SMT

https://doi.org/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. Аналогичный подход можно использовать для формулирования и доказательства полноты процедур трансляции формул в других теориях, таких как теория ограниченных целых с переполнением и теория ограниченной адресной арифметики.

Об авторах

Рафаэль Фаритович САДЫКОВ
Московский государственный университет имени М.В. Ломоносова
Россия
Аспирант кафедры МаТИС механико-математического факультета МГУ


Михаил Усамович МАНДРЫКИН
Институт системного программирования им. В.П. Иванникова РАН
Россия
Младший научный сотрудник, кандидат физико-математических наук


Список литературы

1. T. Nipkow, M. Wenzel, and L.C. Paulson (editors). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science book series, vol. 2283, 2002, 218 p.

2. J. Dawson. Isabelle theories for machine words. Electronic Notes in Theoretical Computer Science, vol. 250, no. 1, 2009, pp. 55-70.

3. D. Babic and M. Musuvathi. Modular arithmetic decision procedure. Technical Report MSR-TR-2005-114, Microsoft Research, 2005.

4. N. Bjørner, A. Blass, Y. Gurevich, and M. Musuvathi. Modular difference logic is hard. Technical Report MSR-TR-2008-140, Microsoft Research, 2008.

5. B.-Y. Wang. On the satisfiability of modular arithmetic formulae. Lecture Notes in Computer Science book series, vol. 4218, 2006, pp. 186–199.

6. S. Böhme. Proof reconstruction for Z3 in Isabelle/HOL. In Proc. of the 7th International Workshop on Satisfiability Modulo Theories (SMT ’09), 2009.

7. S. Böhme and T. Weber. Fast LCF-style proof reconstruction for Z3. Lecture Notes in Computer Science book series, vol. 6172, 2010, pp. 179–194.

8. C. Barrett, P. Fontaine, and C. Tinelli. The SMT-LIB Standard: Version 2.6. Department of Computer Science, The University of Iowa, Technical Report, 2017.

9. R. Sadykov and M. Mandrykin. Completeness of instantiation procedure for bounded linear integer arithmetic. Formalization in Isabelle/HOL. Anailable at: https://forge.ispras.ru/projects/tsmt/repository/, accessed April 2020.

10. D. Greenaway, J. Andronick, and G. Klein. Bridging the gap: Automatic verified abstraction of C. Lecture Notes in Computer Science book series, vol. 7406, 2012, pp. 99–115.

11. Kovásznai G. How Har is Bit-Precise Reasoning? In Proc. of the 10th International Conference on Applied Informatics, 2017. pp. 179-190.


Рецензия

Для цитирования:


САДЫКОВ Р.Ф., МАНДРЫКИН М.У. Верифицированная тактика Isabelle/HOL для теории ограниченных целых на основе инстанцирования и SMT. Труды Института системного программирования РАН. 2020;32(2):107-124. https://doi.org/10.15514/ISPRAS-2020-32(2)-9

For citation:


SADYKOV R.F., MANDRYKIN M.U. Verified Isabelle/HOL tactic for the theory of bounded integers based on quantifier instantiation and SMT. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2020;32(2):107-124. (In Russ.) https://doi.org/10.15514/ISPRAS-2020-32(2)-9



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)