论文标题
经验报告：在CAD开发环境（扩展摘要）中走私一些COQ
Experience Report: Smuggling a Little Bit of Coq Inside a CAD Development Context (Extended Abstract)
论文作者
论文摘要
尽管在关键任务软件的开发中使用正式验证技术已经很好地确定，但在生产大多数其他类型的软件中仍然很少见。我们分享了我们的经验，即在现成的软件开发（尤其是CAD）的背景下，诸如COQ之类的正式验证工具至少在某些情况下是非常有用的。重点是三个主要领域：可以在工业环境中使用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.
