Document Open Access Logo

Automata-Based Verification of Relational Properties of Functions over Algebraic Data Structures

Authors Théo Losekoot, Thomas Genet , Thomas Jensen

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.7.pdf
  • Filesize: 0.92 MB
  • 22 pages

Document Identifiers

Author Details

Théo Losekoot
  • Université de Rennes, IRISA, France
Thomas Genet
  • Université de Rennes, IRISA, France
Thomas Jensen
  • Inria, Université de Rennes, France

Cite As Get BibTex

Théo Losekoot, Thomas Genet, and Thomas Jensen. Automata-Based Verification of Relational Properties of Functions over Algebraic Data Structures. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.FSCD.2023.7

Abstract

This paper is concerned with automatically proving properties about the input-output relation of functional programs operating over algebraic data types. Recent results show how to approximate the image of a functional program using a regular tree language. Though expressive, those techniques cannot prove properties relating the input and the output of a function, e.g., proving that the output of a function reversing a list has the same length as the input list. In this paper, we built upon those results and define a procedure to compute or over-approximate such a relation. Instead of representing the image of a function by a regular set of terms, we represent (an approximation of) the input-output relation by a regular set of tuples of terms. Regular languages of tuples of terms are recognized using a tree automaton recognizing convolutions of terms, where a convolution transforms a tuple of terms into a term built on tuples of symbols. Both the program and the properties are transformed into predicates and Constrained Horn clauses (CHCs). Then, using an Implication Counter Example procedure (ICE), we infer a model of the clauses, associating to each predicate a regular relation. In this ICE procedure, checking if a given model satisfies the clauses is undecidable in general. We overcome undecidability by proposing an incomplete but sound inference procedure for such relational regular properties. Though the procedure is incomplete, its implementation performs well on 120 examples. It efficiently proves non-trivial relational properties or finds counter-examples.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Formal verification
  • Tree automata
  • Constrained Horn Clauses
  • Model inference
  • Relational properties
  • Algebraic datatypes

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Clark Barrett, Igor Shikanian, and Cesare Tinelli. An abstract decision procedure for a theory of inductive data types. Journal on Satisfiability, Boolean Modeling and Computation, 3(1-2):21-46, 2007. Google Scholar
  2. Nikolaj Bjørner, Arie Gurfinkel, Ken McMillan, and Andrey Rybalchenko. Horn clause solvers for program verification. In Fields of Logic and Computation II, pages 24-51. Springer, 2015. Google Scholar
  3. Yohan Boichut, Jacques Chabin, and Pierre Réty. Towards more precise rewriting approximations. J. Comput. Syst. Sci., 104:131-148, 2019. Google Scholar
  4. Koen Claessen, Moa Johansson, Dan Rosén, and Nicholas Smallbone. Tip and isaplanner benchmarks, 2015. URL: https://tip-org.github.io/.
  5. Koen Claessen, Moa Johansson, Dan Rosén, and Nicholas Smallbone. Tip: tons of inductive problems. In International Conference on Intelligent Computer Mathematics, pages 333-337. Springer, 2015. Google Scholar
  6. Hubert Comon, Max Dauchet, Rémi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. Tree Automata Techniques and Applications. 2008. URL: https://hal.inria.fr/hal-03367725.
  7. Lucas Dixon and Jacques Fleuriot. Isaplanner: A prototype proof planner in isabelle. In CADE'03, volume 2741, pages 279-283. Springer, 2003. Google Scholar
  8. Pranav Garg, Christof Löding, P Madhusudan, and Daniel Neider. Ice: A robust framework for learning invariants. In International Conference on Computer Aided Verification, pages 69-87. Springer, 2014. Google Scholar
  9. Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub. Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, 2012. Google Scholar
  10. Erich Grädel. Automatic structures: twenty years later. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 21-34, 2020. Google Scholar
  11. Timothée Haudebourg, Thomas Genet, and Thomas Jensen. Regular Language Type Inference with Term Rewriting. Proceedings of the ACM on Programming Languages, 4(ICFP):1-29, 2020. Google Scholar
  12. Timothée Haudebourg. Automatic Verification of Higher-Order Functional Programs using Regular Tree Languages. PhD thesis, Univ. Rennes1, 2020. Google Scholar
  13. Tirza Hirst and David Harel. More about recursive structures: Descriptive complexity and zero-one laws. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pages 334-347. IEEE, 1996. Google Scholar
  14. R Hodgson Bernard. Théories décidables par automate fini (Decidable theories via finite automata). PhD thesis, Ph.D. thesis Département de Mathématiques et de Statistique, Université de …, 1976. Google Scholar
  15. Bakhadyr Khoussainov and Anil Nerode. Automatic Presentations of Structures. In International Workshop on Logic and Computational Complexity, pages 367-392. Springer, 1994. Google Scholar
  16. Yurii Kostyukov, Dmitry Mordvinov, and Grigory Fedyukovich. Beyond the elementary representations of program invariants over algebraic data types. In Stephen N. Freund and Eran Yahav, editors, PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, pages 451-465. ACM, 2021. Google Scholar
  17. Yuma Matsumoto, Naoki Kobayashi, and Hiroshi Unno. Automata-based abstraction for automated verification of higher-order tree-processing programs. In Asian Symposium on Programming Languages and Systems, pages 295-312. Springer, 2015. Google Scholar
  18. Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, and Ryosuke Sato. Symbolic automatic relations and their applications to SMT and CHC solving. In International Static Analysis Symposium, pages 405-428. Springer, 2021. Google Scholar
  19. Takeshi Tsukada and Hiroshi Unno. Software model-checking as cyclic-proof search. Proceedings of the ACM on Programming Languages, 6(POPL):1-29, 2022. Google Scholar
  20. Hiroshi Unno, Sho Torii, and Hiroki Sakamoto. Automating induction for solving horn clauses. In International Conference on Computer Aided Verification, pages 571-591. Springer, 2017. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact