通向实用演绎验证：来自行业与学术界的定性调查洞见
软件工程
2026-01-26 v2
摘要
演绎验证是确保系统实现预期行为的有效方法。尽管该方法在特定项目中已证明有用且可行，但演绎验证仍未成为主流技术。为此，我们 presenting a study to调查调查实现演绎验证成功应用的关键因素，以及阻碍其更广泛采用的根本问题。我们对来自行业和学术界的30位验证实践者进行半结构化访谈，并系统地采用主题分析方法进行数据分析。除了证实熟悉的挑战（如进行形式证明所需的高水平专业知识外），我们的数据还揭示了若干未被充分探讨的障碍，如证明维护、对自动化的控制不足以及可用性问题。我们进一步利用数据分析结果提取出演绎验证的推动因素和障碍，并为实践者、工具构建者和研究者提出具体建议，包括可用的性、自动化和与现有工作流程集成的原则。
引用
@article{arxiv.2510.20514,
title = {Toward Practical Deductive Verification: Insights from a Qualitative Survey in Industry and Academia},
author = {Lea Salome Brugger and Xavier Denis and Peter Müller},
journal= {arXiv preprint arXiv:2510.20514},
year = {2026}
}