Open Collections

Description

Reasoning about programs requires theories that describe realistic data structures and SMT procedures for theory combination. The standard theory of arrays does not allow integer-indexed arrays to be finite as they are in programs, and the standard Nelson-Oppen theory combination scheme is for disjoint theories, when adding length to arrays causes nondisjointness. These issues have been bypassed by recurring to quantifiers or theories of sequences, jeopardizing decidability or contradicting intuition, since it is counterintuitive that in SMT sequences are finite and arrays infinite. This talk explains these issues and presents a new solution: new theories of arrays, maps, and vectors (i.e., dynamic arrays) with abstract domain, and an extension of the theory combination method CDSAT (Conflict-Driven Satisfiability) to handle nondisjoint theories sharing predicate symbols other than equality. The notion of abstract domain allows one to describe finite arrays, arrays whose equality depend on the starting address in memory, dynamic data structures such as maps and vectors, and more. The generalization of CDSAT from disjoint to predicate-sharing theories preserves gracefully soundness, termination, and completeness. (Joint work with Stéphane Graham-Lengrand and Natarajan Shankar.)