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.

### Citation

Viktor Kuncak and Thomas Wies.
On set-driven combination of logics and verifiers.
Technical Report LARA-REPORT-2009-001, EPFL, February 2009.### BibTex Entry

@techreport{KuncakWies09SetDrivenCombinationofLogicsandVerifiers,
author = {Viktor Kuncak and Thomas Wies},
title = {On Set-Driven Combination of Logics and Verifiers},
institution = {EPFL},
year = 2009,
month = {February},
number = {LARA-REPORT-2009-001},
abstract = {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.
}
}