Representability of invariants of programs with algebraic data type

26 October 2020

First-order logic is a natural way of expressing the properties of computation, traditionally used in various program logics for expressing the correctness properties and certificates. Subsequently, modern methods in the automated inference of program invariants progress towards the construction of first-order definable invariants. Although the first-order representations are very expressive for some theories (LIA, LRA, BV, arrays), they fail to express many interesting properties of algebraic data types (ADTs).

In this talk, three different approaches to represent the inductive invariants of ADT-manipulating programs will be discussed: by first-order formulas, by tree automata, and by first-order formulas with size constraints.

The comparison of the expressive power of these representations based on simple examples will show us how state-of-art invariant inference tools often diverge because of invariant undefinability in the first-order language. We will also talk about the automatic inference of regular invariants of ADT-manipulating programs using finite model finders. An evaluation against state-of-art Horn-solvers will show us that the automata-based representation of invariants is more practical than the one based on first-order logic since invariants are capable of expressing more complex properties of the computation and their automatic construction is less expensive.

Speaker: Yurii Kostyukov

References:

1). Zhang T., Sipma H. B., Manna Z. Decision procedures for recursive data structures with integer constraints //International Joint Conference on Automated Reasoning. โ€“ Springer, Berlin, Heidelberg, 2004. โ€“ ะก. 152-167.

2). Reynolds A. J. Finite model finding in satisfiability modulo theories. โ€“ 2013.

The seminar will be held in google meet on Monday October 26 at 17:30 (google meet room: https://meet.google.com/myu-dhmz-gvu)