IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2010 > Combining Theories with Shared Set Operations
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Ruzica Piskac

lunes 25 de enero de 2010

10:30am Amphitheatre H-1002

Ruzica Piskac, PhD Student, EPFL, Switzerland

Combining Theories with Shared Set Operations


We explore automated reasoning techniques for the non-disjoint combination of theories that share set variables and operations. We are motivated by applications to software analysis, where verification conditions are often expressed in a combination of such theories. The standard Nelson-Oppen result on combining theories does not apply in this setting, because the theories share more than just equalities. We state and prove a new combination theorem and use it to show the decidability of the satisfiability problem for a class of formulas obtained by applying propositional connectives to formulas belonging to:

  • Boolean algebra with Presburger arithmetic (with quantifiers over sets and integers)
  • weak monadic second-order logic over trees (with first and second order quantifiers)
  • two-variable logic with counting quantifiers
  • the Bernays-Schönfinkel-Ramsey class of first-order logic with equality (with ∀^* ∃^* quantifier prefix)
  • the quantifier-free logic of multisets with cardinality constraint We illustrate our result through verification conditions expressing properties of data structures.

This is a joint work with Thomas Wies and Viktor Kuncak.