AI4FM: using AI to aid automation of proof search in Formal Methods

Formal Methods bring to software engineering the level of scientific underpinning familiar in other engineering disciplines. Such methods use specification languages with precise meaning and thus open the possibility of proving that a design (ultimately the implementation) satisfies the specification.Such formal methods have come a long way since their inception and they are now used in applications far more common than the safety-critical systems where they were first deployed. Significant awareness of their potential has come from the use of push-button, post facto, methods that derive from ideas of model checking . The family of methods that can be thought of as top-down have more potential pay-off but are also more challenging for users. Any post-facto method has to face the prospect of incorrect programs - extracting their specifications can be unedifying. Furthermore, an enormous amount of the waste in software development derives from scrap and rework when design errors are discovered after their insertion (but possibly before there is even code to execute). Both post-facto and top-down approaches are important: we choose to address the latter and tackle a key cost in their deployment.In justifying a top-down step of design, the user has to discharge so-called proof obligations . These are small proofs that can often be discharged by an automatic theorem prover. But where they are not discharged automatically, an engineer is faced with the unfamiliar task of constructing a formal proof. Improvements in so-called heuristics can help increase the power of theorem provers. This project aims to use learning techniques from artificial intelligence to record and abstract how experts do proofs in order to increase the proportion of cases where proofs are constructed without (or with minimal) human intervention.

Who will benefit from this research?: The long-term, non-academic beneficiaries of this research will be all users of formal methods in ICT system development. In the shorter term, our prototype system will first be available to users of the Rodin Toolset, e.g. industrial members of the DEPLOY project, such as Bosch, SAP and Siemens. Assuming this leads to a greater uptake of formal methods for ICT system development, then customers of these systems will benefit from more dependable ICT products, i.e. systems that are delivered on-time, on-budget, that meet their specifications and are more easily maintained against an evolving specification. Considering the horrifying statistics associated with the failures of current ICT projects, this would be a major impact. How will they benefit from this research? The potential impact on the practical use of formal methods is huge. It is clear that recalcitrant POs are a major bottleneck in the use of formal methods even within a project like DEPLOY where the industrial partners have already made some commitment to their use. Our tools will increase the level of automation in the use of formal methods. This will result in both a decrease in the required skill level in their use and a decrease in the time take to apply them. Expert interaction will still be required to deal with proof obligations (POs) that are beyond the ability of current theorem proving systems, but this interaction will be limited to an exemplar PO within each family, where a typical family size is 20 POs. The other 19 POs will then be dealt with automatically using the source proof to guide the target proofs. Rare, expensive and highly-skilled proof expertise can then be spread more thinly across a wider range of projects, with less-skilled ICT developers dealing with the automated tools that will deal with the majority of the POs. The savings to users might well amount to a quarter of their costs. With the resulting reduction in costs and time-to-market of formal methods, we would expect a major barrier to their wider uptake to be lifted, and their use to become more routine. What will be done to ensure that they have the opportunity to benefit from this research? Our workplan involves close interaction with several industrial formal-methods users. We will harvest examples from these users to form our development and test sets. This will ensure that we are working on industrially relevant problems. We will embed our prototype in tools, such as the Rodin Toolset, that are being used by these industrial users. This will ensure that our contribution is readily usable by these industrial users. Most importantly, we will engage in a continuous dialogue with these industrial users to ensure that our tools will address their most significant problems. This dialogue will take place not only within this project, but also within sister projects, such as DEPLOY, and our membership of communities, such as UKCRC Grand Challenge 6, on Dependable Systems Evolution and the Verified Systems Initiative . In particular, GC6 and VSI will give us the opportunity to tension our research against related research on a common benchmark of problems. We will, of course, also use all the usual channels of research dissemination: conference and journal publication; seminar, workshop and conference presentations; making software and examples freely available to download; web page with links to publications, etc.; tutorials on our results during the later stages of the project; organising both UK and European workshops on our evolving research, e.g., at Schloss Dagstuhl, involving both industrial and academic researchers; integrating our research results into our teaching, in order to send out a generation of UG and MSc CS students much better equipped to employ FM in their future careers.