AI4FM 2014 will take place as a satellite workshop of FM2014 in Singapore on 12th May 2014
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.
Gudmund Grov have a seminar at Oxford University, as part of the OASIS: The Oxford Advanced Seminar on Informatic Structures seminar series.
Within interactive theorem proving, and in particular conjectures arising from formal methods, many proofs follows a similar pattern. The ability to re-use expert provided proofs to automatically discharge proof within the same “family” could therefore greatly improve automation of such proofs.
An observation we have made is that in order to capture sufficiently generic strategies, properties from both the goals and the underlying proof techniques (tactics) much be captured, which is not well-supported by current tactic languages.
In this talk we introduce a graph based language to represent such proof strategies. Here, the vertices represent the proof techniques, the edges contains goal properties, and evaluation is achieved by “sending” goals along the edges of the graph between the techniques. We will show some properties of this language and outline how we plan to use it to extract strategies from user provided proofs.
Andrius Velykis presents his PhD research (proposal, direction and results) at the Doctoral Symposium at 18th International Symposium on Formal Methods (FM2012) in Paris, France on 27 August 2012.
A Dagstuhl seminar ‘AI meets Formal Software Development’ (Seminar 12271) featured numerous talks on proof automation, learning and formal methods. Most slides and abstracts are available via seminar information Shared Documents service. For convenience, we also list the AI4FM talks and their slides below.
A Dagstuhl seminar ‘AI meets Formal Software Development’ (Seminar 12271) related to the AI4FM project was held on 1-6 July 2012. The seminar was organised by Cliff Jones, Alan Bundy, J Moore and Dieter Hutter. For details, see seminar information page at http://www.dagstuhl.de/12271.
The seminar was an inspiring meeting where industry and academia shared ideas and insights from both formal methods (FM) and artificial intelligence (AI) domains.
Considerable presence of industrial users kept our sights at the right target, namely realistic sizeable problems of interest. A few talks from an AI-only perspective were also illuminating: from the “ecology of machine learning (ML)” to application of ML to problems of proof. A variety of verification tools and techniques was presented: various program verification suites (e.g. Dafny and VCC from Microsoft Research; Perfect developer and ECV from Escher Technologies; GNAT Pro from AdaCore; etc), machine learning tools (e.g. HR, Wikka), theorem provers (e.g. ACL2, ProofPower/Z, Isabelle/HOL, Z/Eves, etc), SAT/SMT solvers (e.g. E, Boggie, Z3, etc.). From the AI4FM project itself, there were presentations on new technology to capture and extract proof process data, as well as ideas for a new high-level proof strategy language used to discover families of proofs from extracted proof process data. Overall, there has been great participation and enthusiasm from the audience with a potential new collaborations to come.
The organisers are preparing a summary report of the event, which will be published in Dagstuhl Reports series and will contain abstracts of all the talks.
Working material from the seminar (slides and abstracts from given talks) is available from Dagstuhl seminar page.
Yuhui Lin presented the joint research with Alan Bundy and Gudmund Grov on using Rippling to automate Event-B invariant preservation proofs. The talk was presented at Workshop on Automated Theory eXploration (ATX 2012), part of the 6th International Conference on Automated Reasoning (IJCAR) in Manchester, UK (30 June - 1 July 2012).
This is an extended version of an earlier work presented at NFM 2012.
Publication presented at the ICML-12 Workshop on Statistical Relational Learning (SRL 2012) in Edinburgh, Scotland on 30 June 2012. An accompanying poster is also available.
Presentation given at 4th NASA Formal Methods Symposium (NFM 2012), Norfolk, Virginia, USA (3-5 April 2012).
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.
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.
The kick-off meeting consisted of 4 sessions totalling 15 talks. Meeting details and slides from the talks are available in meeting information page.