Theorem proving

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

Decision procedures

We have developed decision procedures for following classes of constraints

Combinating reasoning tools

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.