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
- term powers: quantified combination of term algebras (i.e. theory of algebraic data types) and arbitrary decidable theories
Combinating reasoning tools
One technique for combining reasoning tools that we found useful is described in Chapter 4 of Viktor Kuncak's dissertation.
Application
We are applying our decision procedures in software verification, for example in the Jahob system.