I have been mainly focusing on the area of automated solving of quantified Boolean formulas (QBFs). this includes solving general, canonical QBFs but also solving special cases with practical applications. Since the application of SAT solvers has been widely successful in a number of areas, I believe that QBF solvers can have similar impact. At the same time, however, I think that the current understanding of the problem is too shallow and needs to be deepened. Further, we need to pay close attention to the certification of QBF solvers since the and solvers themselves are rather complex programs.