Using AI to aid automation of proof search in Formal Methods

Upcoming events

  • No events.

Events in 2014

Events in 2013

  • AI4FM 2013

    22 July 2013

    AI4FM 2013 has taken place as a satellite workshop of ITP 2013 in Rennes, France on 22 July 2013.

    AI4FM 2013 workshop has brought together researchers from formal methods and AI; it explored the issue of how AI can be used to support the formal software development process, including modelling and proof.

    The workshop consisted of one invited talk: Sharing the Burden of (Dis)proof with Nitpick and Sledgehammer by Jasmin Blanchette, and 9 regular talks. The abstracts of regular talks have been published as a Heriot-Watt Computer Science Technical Report.

    Further information about AI4FM 2013 is available in the workshop website.

Events in 2012

Events in 2011

  • Seminar: Reasoned modelling: towards decision support for system designers

    Wednesday, 30 November 2011, 6:00 pm
    A. Ireland
    The talk will be given as BCS-FACS Evening Seminar Joint event with the London Mathematical Society, London, UK (30 November 2011)

    Abstract: Formal modelling and reasoning are closely related activities. In particular, modelling decisions are typically informed by the analysis of failed proofs. While such analysis is not intellectually challenging from the perspective of mathematical reasoning, it does represent a major barrier to the uptake of formal design methods by mainstream software engineers — whose intuitions lie in modelling and not proof. This problem is exacerbated by the huge number of proof obligations that arise during industrial scale developments.

    Overcoming this barrier would increase the accessibility and productivity of formal design methods, and ultimately the dependability and security of software intensive systems. Andrew Ireland’s talk will describe a programme of research called reasoned modelling which aims to reduce this barrier. In essence he and his collaborators are focused on the development of techniques that abstract away from the complexities of low-level proof obligations, in particular proof-failures, and provide designers with high-level modelling guidance. Their approach is based upon a classification of common modelling patterns. Combined with automatic proof-failure analysis, they use these patterns to automatically generate modelling guidance. Complementing this top-down process, they are experimenting with bottom-up AI theory formation techniques. Specifically, they are exploring how the HR automated theory formation system can be used to increase the flexibility of their modelling patterns. He will report on progress within the context of Event-B, a refinement based modelling formalism. Their longer-term vision for reasoned modelling will also be outlined. This talk is based upon joint work with Gudmund Grov, Maria Teresa Llano and Alison Peas.

  • Talk: Inferring intent from proof attempts: AI4FM project

    19-23 September 2011
    C. B. Jones
    Talk given during the IFIP WG 2.3 meeting 52, Winchester, UK (19-23 April 2011)
  • AI4FM 2011

    28-29 April 2011
    AI4FM 2011 took place at the University of Edinburgh, UK on 28-29 April 2011

    The event spanned 2 days and featured a number of invited talks and short talk sessions. Event details and talk slides are available in the event information page.

  • Talk: AI4FM — how to say "why" in proofs

    19 April 2011
    C. B. Jones
    An invited lecture given at BCTCS 2011 (27th British Colloquium for Theoretical Computer Science), Birmingham (18-21 April 2011)
  • Talk: Productive use of failure in top-down formal methods

    11 April 2011
    Y. Lin, G. Grov and A. Bundy
    Presentation given at ARW 2011 (Automated Reasoning Workshop), Glasgow, Scotland (11-12 April 2011)
  • Talk: Productive use of failure in formal methods

    5 April 2011
    Y. Lin
  • Talk: Some ideas on a proof technique language

    5 April 2011
    G. Grov and L. Dixon
  • Talk: The use of AI to support top-down formal system development

    18 January 2011
    G. Grov
    Seminar given at ETH Zürich, Switzerland (18 January 2011)

Events in 2010

Events in 2009