AI4FM / 2011

The second “AI-meets-Formal Methods” meeting, Edinburgh, 28-29 April 2011

AI4FM 2011

Edinburgh, 28-29 April, 2011

Welcome

Welcome to AI4FM 2011. Following our successful inaugural open meeting held in Newcastle in May 2010, we plan to hold annual meetings where we discuss the project with our collaborators and people interested in it. The AI4FM 2011 event had a similar structure to the Newcastle meeting, where we started the first day with lunch and finished the second day with lunch.

Below you can see a the programme for both days. On the right you can see a map containing relevant venues for the meeting.

Programme

Thursday 28 April 2011 (room 4.31/4.33)

• 12:00: Lunch (room MF2)
• 13:00: Welcome and introduction to the AI4FM projectAlan Bundy (Edinburgh, UK)
• 13:15: About the AI4FM workshop Andrew Ireland (Heriot-Watt, UK)  | Download slides
• 13:30: Models of "Why" Cliff Jones (Newcastle, UK)  | Download slides
• 13:50: Towards a "Repertoire of Reasons" Alan Bundy (Edinburgh, UK)  | Download slides
• 14:10: Elusive "Why": an experiment in capturing proof intent Leo Freitas (Newcastle, UK)  | Download slides
• 14:30: Representing "Whys" — a proof language for Isaplanner Gudmund Grov (Edinburgh, UK)  | Download slides
• 14:50: Discussion: (How to find) "Why" in theorem proving
• 15:40: Coffee and tea break (MF2)
• 16:10: Transforming ProofIain Whiteside (Edinburgh, UK)  | Download slides
• 16:30: Addressing prover and language extensibility issues for Event-BIssam Maamria (Southampton, UK)
• 16:50: Isabelle supports RodinMatthias Schmalz (ETH Zürich, Switzerland)  | Download slides
• 17:10: Invited talk: Abstract program structures for correct refinementMichael Butler (Southampton, UK)  | Download slides Formalisms such as Event-B and action systems provide general rules for refinement of reactive systems, with the rules being based around guarded atomic actions. In this talk, we describe abstract program structures that capture common patterns of refinements involving groups of actions. These structures make it easier to apply the refinement rules of Event-B and action systems. The structures are analogous to program structures for sequential programming but are weaker and more suited to distributed systems.
• 18:00: End
• 18:00-20:00: Wine & food reception (MF2)

Friday 29 April 2011 (room 4.31/4.33)

• 09:00: Invited talk: Intelligent support for systems verificationWerner Stephan (DFKI, Saarbrücken, Germany)  | Download slides The talk presents work on proof automation by heuristics and replay procedures in the Verification Support Environment (VSE). VSE has been applied to commercial software developments for more than 15 years. By examples from code verification and protocol analysis we discuss the achievements of recent years as well as open issues. In particular, we address lemma generation/application and the detection and analysis of failures. Since in formal software development modelling and proof construction often go hand in hand failures are often caused by inadequate formalisations. In the final part we discuss the generality of hierarchical strategies and the problem of adapting them to new situations asking the question of how much of present days paper and pencil work could be supported by a well-engineered assistance system.
• 09:50: What planning can do for formal methodsAndrew Ireland (Heriot-Watt, UK)  | Download slides
• 10:10: Using automated theory formation to discover invariants of Event-B modelsTeresa Llano (Heriot-Watt, UK)  | Download slides
• 10:30: Pattern recognition for coinductive proof treesEkaterina Komendantskaya (Dundee, UK)  | Download slides
• 11:20: Coffee and tea break (MF2)
• 11:50: Invited talk: Yet another theorem prover in distressThierry Lecomte (ClearSy, France)  | Download slides This talk presents some practical proof problems faced during industrial application of the B/Event B formal method through cases coming from railways, aerospace, and microelectronics domains. Different kinds of proof difficulties experimented by human practitioners are exhibited and are put in relation with existing theorem provers.
  Thierry Lecomte has 15 years experience in the development and proof of B software. In the 90's he was in charge of the improvement of Atelier B proof capabilities.
• 12:40: Closing remarks
• 13:00: Lunch (MF2)
• 14:00: End

Venue

All sessions were held in room 4.31/4.33 (4th floor) of the Informatics Forum, University of Edinburgh (see map above). Lunch and coffee/tea breaks as well as the wine/food reception were in Mini Forum 2 (MF2) which is located just outside 4.31/4.33.

Sponsors

This event is sponsored by the Complex Systems Engineering theme of the Scottish Informatics and Computer Science Alliance (SICSA) and the Centre for Intelligent Systems and Their Applications (CISA) at the University of Edinburgh.

Registration

Thanks to the SICSA sponsorship this event is free of charge. However, there are only a limited number of places available, and we apply a first-come-first-served policy.

Registration is achieved by emailing your details to:
Gudmund Grov: ggrov (at) staffmail (dot) ed (dot) ac (dot) uk.

Please register before 28 February 2011.

Accommodation

We do not organise any particular accommodation. However, we can recommend the accommodation listed at:
http://homepages.inf.ed.ac.uk/ldixon/cisa/speaker-info.php

Call for participation

The call for participation is available here.