AI meets Formal Software Development

Motivation

The surge of the commercial use of formal methods continues but a key limiting factor is cost, mostly in terms of necessary skills and time spent during development. Our aim is to reduce such costs and we believe the use of machine learning, automated reasoning and other AI techniques is the way forward to reduce the often repetitive tasks. This seminar will bring together researchers in the AI areas of machine learning, automated reasoning, proof planning, theory formation and theory development with both formal methods researchers and industrial users. The major aim is to combine the efforts of these communities in order to tackle problems arising from commercial use of formal methods. For instance:

• pruning search in theorem proving;
• providing modelling guidance to improve model quality and development time;
• discovering lemmas required in a proof and invent new important concepts;
• learning from existing proofs and proof failures to reduce the burden of proof for similar conjectures;
• adjusting proof processes to take into account "proof engineering" such as the style of proof within different systems;
• discovering counter-examples to reduce time wasted on false conjectures or wrong models; and
• to see if the marriage of AI and formal methods can provide a foundation for new software engineering processes.

Currently, users need mathematical expertise comparable with that of academic researchers in order to (specify formally and) prove properties about specifications and designs. To make formal methods more mainstream, a considerable proportion of manual tasks has to be automated so that experts can focus their attention on problems, such as high-level modelling and abstraction, rather than repetitive on low-level proofs. Hopefully, the required expertise will then be reduced to the point that industrial engineers and domain experts can use formal techniques with minimal need of formal methods experts. We believe that AI has a fundamental role to play in this process, and that discussing the issues above will improve industrial uptake.

The topics of this seminar relate to tool builders, researchers and users of AI and formal methods; overall, there is a strong focus on commercial participants who have some experience with formal methods. The seminar's aim is to amalgamate industrial needs and practical experience, with best-practice advice from both AI and formal methods areas of academia. In particular, the seminar aims to gather information about different areas of interest for industrial users. For example, are their problems mostly within modelling, proof, the development process, or all of these? The aim is further to address industry's main difficulties in using formal methods and an important thread throughout is to identify the challenges and limits of the current use of formal methods within industry.