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

点击翻译按钮获取中文摘要

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.