Автоматический вывод синхронных регулярных инвариантов

Обложка

Цитировать

Полный текст

Открытый доступ Открытый доступ
Доступ закрыт Доступ предоставлен
Доступ закрыт Только для подписчиков

Аннотация

Алгебраические типы данных позволяют представлять сложные структуры данных, поэтому классические методы верификации с помощью вывода индуктивных инвариантов не применимы к программам с такими типами. Основная проблема классических методов состоит в примитивности языка логики, с помощью которой представляются индуктивные инварианты. В данной работе рассмотрены синхронные автоматы над деревьями в качестве альтернативы классическим представлениям инвариантов с помощью логики. Предложен метод автоматического вывода индуктивных инвариантов, представленных синхронными автоматами над деревьями, использующий поиск конечных моделей. Реализация предложенного метода вывела на существующем тестовом наборе на 65% больше инвариантов, чем инструмент, выражающий инварианты с помощью логики и являющийся многократным победителем международных соревнований верификаторов, использующих вывод индуктивных инвариантов.

Об авторах

А. И. Васенина

Санкт-Петербургский государственный университет

Email: a.vasenina@spbu.ru
199034 Санкт-Петербург, Университетская наб., д. 7–9, Россия

Ю. О. Костюков

Санкт-Петербургский государственный университет

Email: y.kostyukov@spbu.ru
199034 Санкт-Петербург, Университетская наб., д. 7–9, Россия

Д. А. Мордвинов

Санкт-Петербургский государственный университет

Email: d.mordvinov@spbu.ru
199034 Санкт-Петербург, Университетская наб., д. 7–9, Россия

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

  1. Filliâtre J.-C., Paskevich A. Why3 – Where Programs Meet Provers // Programming Languages and Systems / Ed. by Matthias Felleisen, Philippa Gardner. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013. P. 125–128.
  2. Refinement types for Haskell / Niki Vazou, Eric L Seidel, Ranjit Jhala et al. // Proceedings of the 19th ACM SIGPLAN international conference on Functional programming. 2014. P. 269–282.
  3. SolCMC: Solidity Compiler’s Model Checker / Leonardo Alt, Martin Blicha, Antti E.J. Hyvärinen, Natasha Sharygina // Computer Aided Verification / Ed. by Sharon Shoham, Yakir Vizel. Cham: Springer International Publishing, 2022. P. 325–338.
  4. SolType: refinement types for arithmetic overflow in solidity / Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri et al. // Proc. ACM Program. Lang. 2022. Vol. 6. No. POPL. 29 p. https://doi.org / 10. 1145 / 3498665
  5. The SeaHorn Verification Framework / Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, Jorge A. Navas // Computer Aided Verification / Ed. by Daniel Kroening, Corina S. Păsăreanu. Cham: Springer International Publishing, 2015. P. 343–361.
  6. Property Directed Self Composition / Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel // Computer Aided Verification / Ed. by Isil Dillig, Serdar Tasiran. Cham: Springer International Publishing, 2019. P. 161–179.
  7. Hoenicke J., Majumdar R., Podelski A. Thread modularity at many levels: a pearl in compositional verification // Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. POPL ‘17. New York, NY, USA: Association for Computing Machinery, 2017. P. 473–485. https://doi.org / 10.1145 / 3009837.3009893
  8. Kostyukov Y., Mordvinov D., Fedyukovich G. Beyond the elementary representations of program invariants over algebraic data types // Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 2021. P. 451–465.
  9. Haudebourg T. Automatic verification of higher-order functional programs using regular tree languages: Ph.D. thesis. 2020. Thèse de doctorat dirigée par Genet, Thomas et Jensen, Thomas Informatique Rennes 1. 2020. http://www.theses.fr / 2020REN1S060
  10. Tree Automata Techniques and Applications / Hubert Comon, Max Dauchet, Rémi Gilleron et al. 2008. P. 262. https://hal. inria. fr / hal-03367725
  11. Kostyukov Y., Mordvinov D., Fedyukovich G. Beyond the Elementary Representations of Program Invariants over Algebraic Data Types // Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI 2021. New York, NY, USA: Association for Computing Machinery, 2021. P. 451–465. https://doi.org / 10.1145 / 3453483.3454055
  12. De Angelis E., Hari Govind V.K. CHCCOMP 2022: Competition Report // Electronic Proceedings in Theoretical Computer Science. 2022. Vol. 373. P. 44–62. http://dx. doi.org / 10.4204 / EPTCS.373.5
  13. Horn Clause Solvers for Program Verification / Nikolaj Bjørner, Arie Gurfinkel, Ken McMillan, Andrey Rybalchenko // Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday / Ed. by Lev D. Beklemishev, Andreas Blass, Nachum Dershowitz et al. Cham: Springer International Publishing, 2015. P. 24–51. https://doi.org / 10.1007 / 978-3-319-23534-9_2
  14. Hojjat H., Rümmer P. The ELDARICA Horn Solver // 2018 Formal Methods in Computer Aided Design (FMCAD). 2018. P. 1–7.
  15. Komuravelli A., Gurfinkel A., Chaki S. SMT-based model checking for recursive programs // Formal Methods in System Design. 2016. Vol. 48. No. 3. P. 175–205.
  16. Bradley Aaron R. SAT-based model checking without unrolling // International Workshop on Verification, Model Checking, and Abstract Interpretation / Springer. 2011. P. 70–87.
  17. de Moura L., Bjørner N. Z3: An Efficient SMT Solver // Tools and Algorithms for the Construction and Analysis of Systems / Ed. by C.R. Ramakrishnan, Jakob Rehof. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008. Р. 337–340.
  18. Hari Govind V.K., Shoham S., Gurfinkel A. Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions // Proceedings of the 2022 ACM-SIGACT Symposium on Principles of Programming Languages. 2022. P. 1–29.
  19. Hojjat H., Rümmer P. The ELDARICA Horn Solver // 2018 Formal Methods in Computer Aided Design (FMCAD). 2018. P. 1–7.
  20. Zhang T., Sipma Henny B., Manna Z. Decision procedures for recursive data structures with integer constraints // International Joint Conference on Automated Reasoning / Springer. 2004. P. 152–167.
  21. Hojjat H., Rümmer P. Deciding and Interpolating Algebraic Data Types by Reduction // 2017 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). 2017. P. 145–152.
  22. ICE: A robust framework for learning invariants / Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider // International Conference on Computer Aided Verification / Springer. 2014. P. 69–87.
  23. Champion A., Kobayashi N., Sato R. HoIce: An ICE-Based Nonlinear Horn Clause Solver // Programming Languages and Systems / Ed. by Sukyoung Ryu. Cham: Springer International Publishing, 2018. P. 146–156.
  24. VeriMAP: A tool for verifying programs through transformations / Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti // International Conference on Tools and Algorithms for the Construction and Analysis of Systems / Springer. 2014. P. 568574.
  25. Solving Horn clauses on inductive data types without induction / Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti // Theory and Practice of Logic Programming. 2018. Vol. 18. No. 3–4. P. 452469.
  26. Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates / Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti // International Joint Conference on Automated Reasoning / Springer. 2020. P. 83–102.
  27. cvc5: A Versatile and Industrial-Strength SMT Solver / Haniel Barbosa, Clark W. Barrett, Martin Brain et al. // Tools and Algorithms for the Construction and Analysis of Systems – 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part I / Ed. by Dana Fisman, Grigore Rosu. Vol. 13243 of Lecture Notes in Computer Science. Springer, 2022. P. 415–442. https://doi.org / 10. 1007 / 978-3-030-99524-9_24
  28. McCune W. Mace4 reference manual and guide // arXiv preprint cs / 0310055. 2003.
  29. Claessen K., Sörensson N. New techniques that improve MACE-style finite model finding // Proceedings of the CADE-19 Workshop: Model Computation-Principles, Algorithms, Applications / Citeseer. 2003. P. 1127.
  30. Slaney J. FINDER: Finite domain enumerator system description // International Conference on Automated Deduction / Springer. 1994. P. 798–801.
  31. Barrett C., Stump A., Tinelli C. The SMT-LIB Standard: Version 2.0 // Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK) / Ed. by A. Gupta, D. Kroening. 2010.
  32. TIP: Tons of Inductive Problems / Koen Claessen, Moa Johansson, Dan Rosen, Nicholas Smallbone // Intelligent Computer Mathematics / Ed. by Manfred Kerber, Jacques Carette, Cezary Kaliszyk et al. Cham: Springer International Publishing, 2015. P. 333–337.

Дополнительные файлы

Доп. файлы
Действие
1. JATS XML
Скачать

© Российская академия наук, 2025

Согласие на обработку персональных данных с помощью сервиса «Яндекс.Метрика»

1. Я (далее – «Пользователь» или «Субъект персональных данных»), осуществляя использование сайта https://journals.rcsi.science/ (далее – «Сайт»), подтверждая свою полную дееспособность даю согласие на обработку персональных данных с использованием средств автоматизации Оператору - федеральному государственному бюджетному учреждению «Российский центр научной информации» (РЦНИ), далее – «Оператор», расположенному по адресу: 119991, г. Москва, Ленинский просп., д.32А, со следующими условиями.

2. Категории обрабатываемых данных: файлы «cookies» (куки-файлы). Файлы «cookie» – это небольшой текстовый файл, который веб-сервер может хранить в браузере Пользователя. Данные файлы веб-сервер загружает на устройство Пользователя при посещении им Сайта. При каждом следующем посещении Пользователем Сайта «cookie» файлы отправляются на Сайт Оператора. Данные файлы позволяют Сайту распознавать устройство Пользователя. Содержимое такого файла может как относиться, так и не относиться к персональным данным, в зависимости от того, содержит ли такой файл персональные данные или содержит обезличенные технические данные.

3. Цель обработки персональных данных: анализ пользовательской активности с помощью сервиса «Яндекс.Метрика».

4. Категории субъектов персональных данных: все Пользователи Сайта, которые дали согласие на обработку файлов «cookie».

5. Способы обработки: сбор, запись, систематизация, накопление, хранение, уточнение (обновление, изменение), извлечение, использование, передача (доступ, предоставление), блокирование, удаление, уничтожение персональных данных.

6. Срок обработки и хранения: до получения от Субъекта персональных данных требования о прекращении обработки/отзыва согласия.

7. Способ отзыва: заявление об отзыве в письменном виде путём его направления на адрес электронной почты Оператора: info@rcsi.science или путем письменного обращения по юридическому адресу: 119991, г. Москва, Ленинский просп., д.32А

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

9. Порядок уничтожения персональных данных при достижении цели их обработки или при наступлении иных законных оснований определяется Оператором в соответствии с законодательством Российской Федерации.

10. Я согласен/согласна квалифицировать в качестве своей простой электронной подписи под настоящим Согласием и под Политикой обработки персональных данных выполнение мною следующего действия на сайте: https://journals.rcsi.science/ нажатие мною на интерфейсе с текстом: «Сайт использует сервис «Яндекс.Метрика» (который использует файлы «cookie») на элемент с текстом «Принять и продолжить».