The software industry is still in its infancy to widely adopt program verification tools as part of their daily software engineering processes. One key challenge is that many of today’s program verifiers intent to cover numerous bug classes and are therefore manually configurable to support users with their varying verification projects. However, configuring a program verifier for a given problem requires extensive expertise, as an ill-chosen configuration may either unnecessarily slow down the verification process or even hinder a successful verification at all. In particular for configurable program verifiers based on theorem proving, this problem is barely addressed by current research. To lessen the configuration burden that typical software developers consequently face, we present GUIDO, a framework incorporating statistical hypothesis testing to compute promising configurations automatically. With GUIDO, domain experts, such as tool builders, channel their knowledge by formalizing hypotheses about the impact of choosing configuration options and let normal users, such as developers, benefit from it. We applied GUIDO to the state-of-the-art deductive program verifier KeY on 94 specification cases from four existing verification benchmarks. Our results show that GUIDO’s approach outperforms both the default configuration and a random selection process, leading to a reduction of the verification effort while simultaneously decreasing the number of failed proof attempts.