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