Proceedings paper

Farkas-Based Tree Interpolation
S. Asadi, M. Blicha, A. Hyvärinen, G. Fedyukovich, N. Sharygina
Proceedings of 27th Static Analysis Symposium

Linear arithmetic over reals (LRA) underlies a wide rangeof SMT-based modeling approaches, and, strengthened with Craig interpolation using Farkas’ lemma, is a central tool for efficient over-approximation. Recent advances in LRA interpolation have resulted ina range of promising interpolation algorithms with so far poorly understood properties. In this work we study the Farkas-based algorithms with respect to tree interpolation, a practically important approach where a set of interpolants is constructed following a given tree structure. We classify the algorithms based on whether they guarantee the tree interpolation property, and present how to lift a recently introduced approach producing conjunctive LRA interpolants to tree interpolation in the quantifier-free LRA fragment of first-order logic. Our experiments show that the standard interpolation and the approach using conjunctive interpolants are complementary in tree interpolation, and suggest that their combination would be very powerful in practice.

    title = {{Farkas-Based Tree Interpolation}},
    author = {Asadi, Sepideh and Blicha, Martin and Hyvärinen, Antti E. J. and Fedyukovich, Grigory and Sharygina, Natasha},
    year = {2020},
    booktitle = {{Proceedings of 27th Static Analysis Symposium}},
    url = {},