论文标题
正式的正式方法：与开发人员见面
Towards making formal methods normal: meeting developers where they are
论文作者
论文摘要
对软件的正式验证有点适合利基活动：仅应用于最关键或最关键的安全软件，通常仅由专业验证工程师执行。本文考虑是否可以通过将形式方法与开发人员的现有实践和工作流程相结合来增加对形式方法的采用。 我们认为，通过提出普遍的正式方法论点，即正确性比工程团队意识到的更为重要，我们不认为采用广泛的采用。相反，我们的重点是使程序员能够有效利用正式验证工具和技术需要做的事情。我们通过考虑如何制作验证工具来实现这一目标，以满足开发人员的需求并适合其现有开发生命周期。我们提出了一个在十年内提高采用率两个数量级的目标，这是通过确保投入的开发人员时间的积极的“每周成本效益”比率。
Formal verification of software is a bit of a niche activity: it is only applied to the most safety-critical or security-critical software and it is typically only performed by specialized verification engineers. This paper considers whether it would be possible to increase adoption of formal methods by integrating formal methods with developers' existing practices and workflows. We do not believe that widespread adoption will follow from making the prevailing formal methods argument that correctness is more important than engineering teams realize. Instead, our focus is on what we would need to do to enable programmers to make effective use of formal verification tools and techniques. We do this by considering how we might make verification tooling that both serves developers' needs and fits into their existing development lifecycle. We propose a target of two orders of magnitude increase in adoption within a decade driven by ensuring a positive `weekly cost-benefit' ratio for developer time invested.
