Automatic inference of synchronous regular invariants

Мұқаба

Дәйексөз келтіру

Толық мәтін

Ашық рұқсат Ашық рұқсат
Рұқсат жабық Рұқсат берілді
Рұқсат жабық Тек жазылушылар үшін

Аннотация

Algebraic data types allow representing complex data structures, thus classical verification methods relying on inductive invariant inference are not applicable to programs with such types. The main problem with classical methods is the weakness of the first-order logic language used to represent inductive invariants. In this paper, synchronous automata over trees are considered as an alternative to classical representations of invariants using first-order logic. A method for automatic inductive invariant inference represented by synchronous automata over trees is proposed. The method uses finite-model finding. The implementation of the proposed method finds 65% more invariants than a first-order logic based tool, which is an annual winner of an international verifier competition, on an existing benchmark.

Авторлар туралы

A. Vasenina

Saint Petersburg State University

Email: a.vasenina@spbu.ru
7–9 Universitetskaya Embankment, St Petersburg, Russia, 199034

Y. Kostyukov

Saint Petersburg State University

Email: y.kostyukov@spbu.ru
7–9 Universitetskaya Embankment, St Petersburg, Russia, 199034

D. Mordvinov

Saint Petersburg State University

Email: d.mordvinov@spbu.ru
7–9 Universitetskaya Embankment, St Petersburg, Russia, 199034

Әдебиет тізімі

  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
Жүктеу

© Russian Academy of Sciences, 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») на элемент с текстом «Принять и продолжить».