一句话：通过扎根理论访谈14名Dafny用户，分析自动主动验证对大型项目开发的影响与采纳机会。
自动主动验证器（如Dafny）借助SMT自动化，旨在让非专家也能使用形式化方法；然而在实际软件开发中，其应用仍不广泛，因为实践所需投入巨大。本文对14名经验丰富的Dafny用户进行访谈，了解他们在大型项目中使用该工具的经验，并采用扎根理论对访谈材料进行系统分析。研究目标是识别自动主动验证如何影响软件开发过程，并发现简化其使用、从而扩大形式化验证在软件开发中采纳的机会。
Auto-active verifiers like Dafny aim to make formal methods accessible to non-expert users through SMT automation. However, despite the automation and other programmer-friendly features, they remain sparsely used in real-world software development, due to the significant effort required to apply them in practice. We interviewed 14 experienced Dafny users about their experiences using it in large-scale projects. We apply grounded theory to analyze the interviews to systematically identify how auto-active verification impacts software development, and to identify opportunities to simplify the use, and hence, expand the adoption of verification in software development.
@article{paperbot2905,
title = {On the Impact of Formal Verification on Software Development},
author = {Eric Mugnier and Yuanyuan Zhou and Ranjit Jhala and Michael Coblenz},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763181}
}