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.

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.
}
}