经验报告：在CAD开发环境中悄然引入少量Coq（扩展摘要）
编程语言
2020-07-03 v1
摘要
尽管形式化验证技术在任务关键型软件开发中已得到成熟应用，但在大多数其他类型软件的生产中仍属罕见。我们分享的经验表明，诸如Coq的形式化验证工具在现成软件开发（尤其是CAD）中，至少在某些场合下非常有用且实用。重点在于三个主要方面：可在工业环境中启用Coq的因素；Coq能带来优势的一些典型任务示例；在标准开发流程中集成Coq时需要克服的问题示例——以及一些非问题。
引用
@article{arxiv.2007.00695,
title = {Experience Report: Smuggling a Little Bit of Coq Inside a CAD Development Context (Extended Abstract)},
author = {Dimitur Nikolaev Krustev},
journal= {arXiv preprint arXiv:2007.00695},
year = {2020}
}
备注
Submitted to Coq Workshop 2020