2022/04/25 by Silvio Ghilardi, Ghilardi, Silvio, Alessandro Gianola +5
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO
paper · pdf · doi:10.48550/arxiv.2204.11771
arXiv admin note: text overlap with arXiv:2010.07082
arxiv created 2022/04/25 · arxiv updated 2022/04/26
Interpolation is an essential tool in software verification, where first-order theories are used to constrain datatypes manipulated by programs. In this paper, we introduce the datatype theory of contiguous arrays with maxdiff, where arrays are completely defined in their allocation memory and for which maxdiff returns the max index where they differ. This theory is strictly more expressive than the array theories previously studied. By showing via an algebraic analysis that its models strongly amalgamate, we prove that this theory admits quantifier-free interpolants and, notably, that interpolation transfers to theory combinations. Finally, we provide an algorithm that significantly improves the ones for related array theories: it relies on a polysize reduction to general interpolation in linear arithmetics, thus avoiding impractical full terms instantiations and unbounded loops.