Events
Upcoming events
-
Seminar: Reasoned modelling: towards decision support for system designers
Wednesday, 30 November 2011, 6:00 pmThe 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.
-
Dagstuhl seminar 12271: AI meets Formal Software Development
1-6 July 2012A Dagstuhl seminar ‘AI meets Formal Software Development’ (Seminar 12271) related to the AI4FM project will held on 1-6 July 2012. The seminar is organised by Cliff Jones, Alan Bundy, J Moore and Dieter Hutter. For details, see seminar information page at http://www.dagstuhl.de/12271.
Events in 2011
-
Talk: Inferring intent from proof attempts: AI4FM project
19-23 September 2011Talk given during the IFIP WG 2.3 meeting 52, Winchester, UK (19-23 April 2011) -
AI4FM 2011
28-29 April 2011AI4FM 2011 took place at the University of Edinburgh, UK on 28-29 April 2011The 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 2011An 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 2011Presentation given at ARW 2011 (Automated Reasoning Workshop), Glasgow, Scotland (11-12 April 2011) -
Talk: Productive use of failure in formal methods
5 April 2011Presented at CIAO/Automatheo 2011 (Workshop on Automated Mathematical Reasoning and Theory Exploration), Oxford (5-6 April 2011) -
Talk: Some ideas on a proof technique language
5 April 2011Presented at CIAO/Automatheo 2011 (Workshop on Automated Mathematical Reasoning and Theory Exploration), Oxford (5-6 April 2011) -
Talk: The use of AI to support top-down formal system development
18 January 2011Seminar given at ETH Zürich, Switzerland (18 January 2011)
Events in 2010
-
Talk: Learning from an expert's proof
16 November 2010Publication presented at UV10 (Usable Verification) workshop, Microsoft Research at Redmond, Washington, USA (15-16 November 2010) -
Talk: A (very) small experiment in Event-B rippling
22 September 2010Presentation given at Rodin User and Developer Workshop 2010, Düsseldorf, Germany (22 September 2010) -
Talk: Formal Modelling of Separation Kernel Components
2 September 2010A research paper presentation given at ICTAC 2010 conference, Natal, Brazil (2 September 2010)View as interactive Prezi presentation | Download slides as PDF | Read the publication | Visit ICTAC 2010 website -
Talk: AI4FM — A new project seeking challenges!
19 August 2010Presented at Tools & Experiments workshop at VSTTE 2010 conference, Edinburgh (19 August 2010) -
Talk: Abstractions before proofs
20 July 2010Cliff B Jones was an invited speaker at VERIFY-2010 (6th International Verification Workshop), part of Federated Logic Conference (FLoC), Edinburgh (20 July 2010) -
Talk: Ideas for a high-level proof strategy language: starting the AI4FM project
14 July 2010Presented at AFM10 (Automated Formal Methods) workshop, part of Federated Logic Conference (FLoC), Edinburgh (14 July 2010) -
AI4FM kick-off meeting
AI4FM kick-off meeting took place at Newcastle University on 20-21 May, 2010The kick-off meeting consisted of 4 sessions totalling 15 talks. Meeting details and slides from the talks are available in meeting information page.
-
Talk: Another way to use AI ideas to support formal methods
6 May 2010Presented as an Annual Distinguished Seminar at Software Technology Research Laboratory, De Montfort University, Leicester (6 May 2010)
Events in 2009
-
Talk: Learning from experts to aid the automation of proof search
Presented at AVoCS'09, Gregynog, Wales (September, 2009) -
Talk: AI4FM
Presented at Schloss Dagstuhl workshop on Refinement Based Methods, Schloss Dagstuhl, Germany (September, 2009)
