On Set-Driven Combination of Logics and Verifiers

We explore the problem of automated reasoning about the non-disjoint combination of logics that share set variables and operations. We prove a general combination theorem, and apply it to show the decidability for the quantifier-free combination of formulas in WS2S, two-varible logic with counting, and Boolean Algebra with Presburger Arithmetic. Furthermore, we present an over-approximating algorithm that uses such combined logics to synthesize universally quantified invariants of infinite-state systems. The algorithm simultaneously synthesizes loop invariants of interest, and infers the relationships between sets to exchange the information between logics. We have implemented this algorithm and used it to prove detailed correctness properties of operations of linked data structure implementations.