Lessons from Formally Verified Deployed Software Systems (Extended version)
arxiv(2023)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要