Research

The Theoretical Computer Science Group is working on various problems related to logic and verification, including:

• Properties of logics, theories, and fragments
• Development of calculi, effective proof or decision procedures, and the implementation of such methods as theorem provers and SMT solvers
• Methods for Craig interpolation and quantifier elimination
• Connection of logic and automata methods
• Specification languages and intermediate languages for program verification