Representability of invariants of programs with algebraic data type
Firstorder 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 firstorder definable invariants. Although the firstorder 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 ADTmanipulating programs will be discussed: by firstorder formulas, by tree automata, and by firstorder formulas with size constraints.
The comparison of the expressive power of these representations based on simple examples will show us how stateofart invariant inference tools often diverge because of invariant undefinability in the firstorder language. We will also talk about the automatic inference of regular invariants of ADTmanipulating programs using finite model finders. An evaluation against stateofart Hornsolvers will show us that the automatabased representation of invariants is more practical than the one based on firstorder 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. โ ะก. 152167.
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/myudhmzgvu)
 About seminars

23 November 2020Efficient Fair Conjunction for StructurallyRecursive Relations

16 November 2020SourceTracking Unification via ContextFree Path Querying

9 November 2020Relational Synthesis for Pattern Matching

2 November 2020Definitional ProofIrrelevance without K

26 October 2020Representability of invariants of programs with algebraic data type