Document

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

## File

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

## Cite As

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

## 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.
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.
3. Yohan Boichut, Jacques Chabin, and Pierre Réty. Towards more precise rewriting approximations. J. Comput. Syst. Sci., 104:131-148, 2019.
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.
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.
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.
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.
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.
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.
12. Timothée Haudebourg. Automatic Verification of Higher-Order Functional Programs using Regular Tree Languages. PhD thesis, Univ. Rennes1, 2020.
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.
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.
15. Bakhadyr Khoussainov and Anil Nerode. Automatic Presentations of Structures. In International Workshop on Logic and Computational Complexity, pages 367-392. Springer, 1994.
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.
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.
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.
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.
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.
X

Feedback for Dagstuhl Publishing