GUIDO: Automated Guidance for the Configuration of Deductive Program Verifiers

摘要

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 verification 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 deductive program verifiers, this problem is barely addressed by current research. We propose GUIDO, a framework incorporating statistical hypothesis testing to compute promising configurations automatically. With GUIDO, domain experts channel their knowledge by formalizing hypotheses about the impact of choosing configuration options and let normal developers benefit.