DTacs - Program Verifier Tactics : Reducing the Development Time for Program Verifiers with re-usable Verification Strategies

软件与我们接触或依赖的几乎所有数字产品交织在一起：从通信、娱乐和消费电子产品，到铁路、空气控制、汽车、金融、国防、国家基础设施和医疗保健系统。这类软件的可靠性仍然是一个重大挑战。2002年，据估计，软件错误给美国经济造成了590亿美元的损失；最近的估计表明，全球每年的损失超过3000亿美元。因此，可靠性是商业产品的一个关键差异化因素。无论谁能以经济高效的方式解决可靠性挑战，都将获得重大优势。用于确保可靠性的传统技术是以测试为基础的；而这可能相当于开发时间的一半。尽管如此，测试的一个基本问题是，输入和条件的所有组合都不可行。软件工程的正式方法使用数学来确保可靠性。与传统测试技术相比，这些技术的优势在于，可以证明软件对于输入和条件的所有组合都是正确的。这是使用数学的结果，提高了可靠性和产品质量。然而，这些方法的共同瓶颈是定理证明技能的有限可用性和工具提供的自动化程度的缺乏。因此，当它们应用于安全和关键任务系统等利基市场之外时，它们往往会受到开发时间和成本增加的影响。程序验证是一种正式的软件工程技术，其源代码与所需行为的正式规范相结合。数学被用来证明程序满足其规格。最近，出现了一波新的程序验证器，其中隐藏了潜在的数学知识。程序员熟悉的技能被用来指导程序文本中的证明，而不是定理证明技能；消除了与定理证明者相关的“技能障碍”，为软件工程师创造了一种更容易理解的学科。尽管如此，一个开放的挑战是减少完成程序验证所需的指导量--这是一个在程序验证成为可行的、具有成本效益的主流软件工程学科之前必须解决的挑战。该建议通过使软件工程师能够将用于指导校样的模式直接作为特殊程序在程序文本中进行编码，从而解决了自动化挑战。因此，通常由试错过程产生的低级别和重复的细节可以被更高级别的基础模式所取代。这些可以重复用于类似的任务，将用户从低级和重复的搜索任务中解放出来。由于一个模式只需要开发一次，因此需要的指导更少--增加了自动化，减少了开发时间和成本。程序验证器中用于编写程序和指导证明的语言将得到扩展，使软件工程师也能够对他们的验证模式进行编码。扩展应尽可能少，以避免因必须克服新的技能障碍而降低可访问性。这种语言的发展需要对用户如何引导节目审核者有新的理解。我们将重点放在Dafny程序验证器上；重新设计一些可用的Dafny案例研究中使用的开发流程；以及从头开始开发和验证新程序。在这两种情况下，验证过程的每个步骤都将被捕获，从而创建一个验证模式目录。在这个目录的基础上，Dafny内部使用的语言将被扩展为一种新的特殊方法，称为‘DTac’(Dafny Tack)。验证模式将被编码为DTAC。自动化将通过开发一种名为Tacny的新工具来实现，该工具可以读取DTAC并将其应用于其他Dafny程序，以自动进行验证。

Software is woven into just about everything digital that we touch or depend upon: from communications, entertainment and consumer electronics - to railway, air-control, automotive, finance, defence, national infrastructure and health-care systems. The dependability of such software remains a major challenge. In 2002 it was estimated that software mistakes cost the US economy $59 Billion; more recent estimates have suggested an annual cost of more than $300 Billion worldwide. Dependability is therefore a key differentiator in commercial products. Whoever can cost-effectively crack the dependability challenge will have a major advantage.Conventional techniques used to ensure dependability are based around testing; and this can amount to half of the development time. Still, a fundamental problem of testing is that all combinations of inputs and conditions are not feasible. Formal approaches to software engineering use mathematics to ensure dependability. These have the advantage over conventional testing techniques that the software can be proven correct for all combinations of inputs and conditions. This is a result of using mathematics, and increases both the dependability and product quality. However, common bottlenecks of these approaches are limited availability of theorem proving skills and lack of automation provided by tools. Therefore they have often suffered from increased development time and costs when applied beyond niche markets such as safety and mission critical systems.Program verification is a formal software engineering technique where the source code is combined with a formal specification of desired behaviour. Mathematics is used to prove that the program satisfies its specification. Recently, there has been a wave of new program verifiers, where the underlying mathematics is hidden. Skills familiar to programmers are used to guide the proof in the program text rather than theorem proving skills; removing the "skill-barrier" associated with theorem provers and creating a more accessible discipline for a software engineer. Still, an open challenge is to reduce the amount of guidance that is required to complete the verification of a program - a challenge that has to be solved before program verification becomes a viable cost-effective mainstream software engineering discipline. This proposal addresses the automation challenge by enabling software engineers to encode patterns used to guide proofs directly in the program text as special programs. As a result, low-level and repetitive details, often resulting from a trial-and-error process, can be replaced by a higher-level underlying pattern. These can be re-used for similar tasks, liberating users from low-level and repetitive search tasks. As a pattern only needs to be developed once, less guidance will be needed - increasing automation and reducing development time and cost.The language used to write programs and guide proofs within a program verifier will be extended to enable software engineers to also encode their verification patterns. The extension should be as minimal as possible, to avoid reducing accessibility with new skill-barriers that have to be overcome. The development of such language requires a new understanding of how users guide program verifiers. We will focus on the Dafny program verifier; re-engineering the development process used in a selection of the available Dafny case studies; and developing and verifying new programs from scratch. In both cases, each step of the verification process will be captured, creating a catalogue of verification patterns. Based on this catalogue the language used within Dafny will be extended with a new special method called a `DTac' (Dafny Tactic). A verification pattern will be encoded as a DTac. Automation will be achieved by developing a new tool called Tacny that can read DTacs and apply them to other Dafny programs to automate the verification.