Our goal is to develop techniques for proving formulas from expressive logics, which arise in domains such as software verification.

We are developing

• decision procedures for specialized theories
• techniques for combining different reasoning tools

We have developed decision procedures for following classes of constraints

• term powers: quantified combination of term algebras (i.e. theory of algebraic data types) and arbitrary decidable theories
• sets with cardinality constraints
• multisets with cardinality constraints
• linear arithmetic with star operators

One technique for combining reasoning tools that we found useful is described in Chapter 4 of Viktor Kuncak's dissertation.

We are applying our decision procedures in software verification, for example in the Jahob system.