Research publications

Publication listing for 2011

  • Productive use of failure in top-down formal methods

    A. Bundy, G. Grov, and Y. Lin
    In proceedings of ARW 2011 (Automated Reasoning Workshop).

    Abstract: Proof obligations (POs) arise when applying formal methods (FMs). The undischarged POs can become a bottleneck in the use of FMs in industry. The work we proposed here, as a part of AI4FM project, aims at increasing the proportion of discharged POs by analysing failed proofs and related patches to classify POs as families and construct proof strategies, which can be used to guide proof search for the POs in the same families.

Publication listing for 2010

  • Learning from an expert's proof

    L. Freitas and C. B. Jones
    In proceedings of UV10 (Usable Verification) workshop.

    Abstract: This position paper outlines the background and current approaches taken within AI4FM, a 4-year research project aimed at combining AI methodologies to aid proof discovery of certain families of interest. Namely, those repeated proofs often appearing in the application of verification to industrial applications.

  • A small experiment in Event-B rippling

    G. Grov, A. Bundy, and L. Dixon
    In proceedings of AVoCS 2010 and Rodin User and Developer Workshop 2010.

  • AI4FM — A new project seeking challenges!

    G. Grov and C. B. Jones
    In proceedings of Tools & Experiments workshop at VSTTE 2010.

    Abstract: The "proof obligations" generated from many formal method tend to be simple and can often be discharged by modern automatic theorem provers or SMT systems. However, those proof tasks that need hand –or interactive– intervention present a barrier to the use of formal methods. Theorem proving was one of the earliest challenges addressed by researchers in the area of Artificial Intelligence and enormous progress has been made in the provision of general purpose heuristics. The approach in the recently started AI4FM project is different: we hope to devise a system that will learn from an expert user how they tackle one interactive proof and then apply the discovered high-level strategy to other related proof tasks. We are fortunate in having access to many such problems through the DEPLOY project but are aware of the dan- gers of devising an overly specific approach. This short paper appeals for challenge problems from other sources.

  • Formal Modelling of Separation Kernel Components

    A. Velykis and L. Freitas
    In proceedings of 7th International Colloquium on Theoretical Aspects of Computing (ICTAC 2010), LNCS 6255.

    Abstract: Separation kernels are key components in embedded applications. Their small size and widespread use in high-integrity environments make them good targets for formal modelling and verification. We summarise results from the mechanisation of a separation kernel scheduler using the Z/Eves theorem prover. We concentrate on key data structures to model scheduler operations. The results are part of an experiment in a Grand Challenge in software verification, as part of a pilot project in verified OS kernels. The project aims at creating a mechanised formal model of kernel components that gets refined to code. This provides a set of reusable components, proof strategies, and general lemmas. Important findings about properties and requirements are also discussed.

  • Ideas for a high-level proof strategy language

    C. B. Jones, G. Grov, and A. Bundy
    In proceedings of Fifth Automated Formal Methods workshops (AFM'10) — In association with Computer-Aided Verification (CAV) 2010, part of the Federated Logic Conference (FLoC).

    Abstract: Finding ways to prove theorems mechanically was one of the earliest challenges tackled by the AI community. Notable progress has been made but there is still always a limit to any set of heuristic search techniques. From a proof done by human users, we wish to find out whether AI techniques can also be used to learn from a human user. AI4FM (Artificial Intelligence for Formal Methods) is a four-year project that starts officially in April 2010. It focuses on helping users of "formal methods" many of which give rise to proof obligations that have to be (mechanically) verified (by a theorem prover). In industrial-sized developments, there are often a large number of proof obligations and, whilst many of them succumb to similar proof strategies, those that remain can hold up engineers trying to use formal methods. The goal of AI4FM is to learn enough from one manual proof, to discharge proof obligations automatically that yield to similar proof strategies. To achieve this, a high-level (proof) strategy language is required, and in this paper we outline some ideas of such language, and towards extracting them.

  • The AI4FM approach for proof automation within formal methods — A Grand Challenge 6 "Dependable Systems Evolution" project

    G. Grov, A. Bundy, C. B. Jones, and A. Ireland
    In UKCRC Submissions to Grand Challenges in Computing Research 2010 GCCR’10 (April, 2010)

Publication listing for 2009

  • An outline of a proposed system that learns from experts how to discharge proof obligations automatically

    A. Bundy, G. Grov, and C. B. Jones
    Extended abstract to appear in Dagstuhl proceedings on Refinement Based Methods (Seminar 09381; September, 2009).

  • Learning from experts to aid the automation of proof search

    A. Bundy, G. Grov, and C. B. Jones
    Short contribution to AVoCS’09

    Abstract: Most formal methods give rise to proof obligations (POs) which are putative lemmas that need proof. Discharging these POs can become a bottleneck in the use of formal methods in practical applications. It is our aim to increase the repertoire of techniques for reducing this bottleneck by tackling learning from proof attempts. In many cases where a correct PO has not been discharged, an expert can easily see how to complete a proof. We believe that it would be acceptable to rely on such expert intervention to do one proof if this would enable a system to kill off others "of the same form".

Posters

Theses

  • Extending the proof methods and critics of a proof planner

    MSc thesis in Cognitive Science by Daniel Raggi (School of Informatics, Univeristy of Edinburgh, 2011)

  • A study in the use of Event-B for system development from a software engineering viewpoint

    MSc thesis by Sasan Padidar (School of Informatics, Univeristy of Edinburgh, 2010)

AI4FM documents

  • Case for support — AI4FM research project proposal

    C. B. Jones, A. Bundy, and A. Ireland

Background information

The following resources have not been published as part of the AI4FM project. They are included as background information supporting the ideas behind the research.