从正式验证部署软件系统中汲取的经验（扩展版）
Lessons from Formally Verified Deployed Software Systems (Extended version)
AI总结：
本文通过分析多个已部署的正式验证系统，探讨了形式验证技术在实际软件开发中的应用现状、技术实现及行业启示。
摘要：
形式软件验证技术取得了显著进展，但这种技术在实际软件开发中到底带来了多少好处？关于使用机械检查正确性证明来构建系统的实用性仍存在很大分歧。这种前景是否仅限于少数昂贵、生命攸关的项目，还是可以应用于软件行业的广泛领域？为了回答这个问题，本文调查了各种应用领域中已产生正式验证系统并实际部署的项目。它考虑了所使用的技术、应用的验证形式、取得的结果，以及软件行业应从中吸取的教训，以了解其能否从形式验证技术和工具中受益。注：本版本是扩展文章，涵盖了所有相关系统。还有一篇较短的版本，仅涵盖部分系统（见https://doi.org/10.1145/3785652）.
英文摘要：
The technology of formal software verification has made spectacular advances, but how much does it actually benefit the development of practical software? Considerable disagreement remains about the practicality of building systems with mechanically-checked proofs of correctness. Is this prospect confined to a few expensive, life-critical projects, or can the idea be applied to a wide segment of the software industry? To help answer this question, the present survey examines a range of projects, in various application areas, that have produced formally verified systems and deployed them for actual use. It considers the technologies used, the form of verification applied, the results obtained, and the lessons that the software industry should draw regarding its ability to benefit from formal verification techniques and tools. Note: this version is the extended article, covering all the systems identified as relevant. A shorter version, covering only a selection, is also available (see https://doi.org/10.1145/3785652).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
