Deductive verification is an effective method to ensure that a given system exposes the intended behavior. In spite of its proven usefulness and feasibility in selected projects, deductive verification is still not a mainstream technique. To pave the way to widespread use, we present a study investigating the factors enabling successful applications of deductive verification and the underlying issues preventing broader adoption. We conducted semi-structured interviews with 30 practitioners of verification from both industry and academia and systematically analyzed the collected data employing a thematic analysis approach. Beside empirically confirming familiar challenges, e.g., the high level of expertise needed for conducting formal proofs, our data reveal several underexplored obstacles, such as proof maintenance, insufficient control over automation, and usability concerns. We further use the results from our data analysis to extract enablers and barriers for deductive verification and formulate concrete recommendations for practitioners, tool builders, and researchers, including principles for usability, automation, and integration with existing workflows.

翻译：演绎验证是确保给定系统展现预期行为的有效方法。尽管在特定项目中已证明其有用性和可行性，演绎验证仍未成为主流技术。为推广其广泛应用，本研究通过调查探究了促成演绎验证成功应用的因素及阻碍其广泛采纳的深层问题。我们对来自工业界和学术界的30位验证实践者进行了半结构化访谈，并采用主题分析方法对收集的数据进行了系统分析。除了实证确认已知挑战（如开展形式化证明所需的高水平专业知识）外，我们的数据还揭示了若干尚未充分探索的障碍，包括证明维护、对自动化控制不足以及可用性问题。我们进一步利用数据分析结果，提炼出演绎验证的促进因素与阻碍因素，并为实践者、工具开发者和研究者提出具体建议，包括可用性原则、自动化原则以及与现有工作流程的集成原则。