经验报告：在CAD开发环境中走私一点Coq（扩展摘要）
Experience Report: Smuggling a Little Bit of Coq Inside a CAD Development Context (Extended Abstract)
摘要：
虽然形式化验证技术在关键任务软件的开发中得到了很好的应用，但在大多数其他类型的软件的生产中仍然很少见。我们分享我们的经验，一个形式化验证工具，如Coq可以是非常有用和实用的现成的软件开发的背景下- CAD特别是-至少在某些场合。重点是3个主要领域：可以在工业环境中使用Coq的因素; Coq可以提供优势的任务的一些典型示例;将Coq集成到标准开发过程中时需要克服的问题和一些非问题的示例。
英文摘要：
While the use of formal verification techniques is well established in the development of mission-critical software, it is still rare in the production of most other kinds of software. We share our experience that a formal verification tool such as Coq can be very useful and practical in the context of off-the-shelf software development -- CAD in particular -- at least in some occasions. The emphasis is on 3 main areas: factors that can enable the use of Coq in an industrial context; some typical examples of tasks, where Coq can offer an advantage; examples of issues to overcome - and some non-issues - when integrating Coq in a standard development process.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
