  Many verification and synthesis approaches rely on solving techniques for
quantified Boolean formulas (QBF). Consequently, solution witnesses, in the
form of Boolean functions, become more and more important as they represent
implementations or counterexamples. We present a recursive counterexample
guided abstraction and refinement algorithm (CEGAR) for solving and certifying
QBFs that exploits structural reasoning on the formula level. The algorithm
decomposes the given QBF into one propositional formula for every block of
quantifiers that abstracts from assignments of variables not bound by this
quantifier block. Further, we show how to derive an efficient certification
extraction method on top of the algorithm. We report on experimental evaluation
of this algorithm in the solver QuAbS (Quantified Abstraction Solver) which won
the most recent QBF competition (QBFEVAL'18). Further, we show the
effectiveness of the certification approach using synthesis benchmarks and a
case study for synthesizing winning strategies in Petri Games.
