Integrated formal methods - 9th International Conference, IFM 2012

This volume contains the proceedings of iFM 2012, the 9th International Conference on Integrated FormalMethods, held during June 18-21, 2012, in Pisa, Italy, jointly with ABZ 2012, the 3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, in honor of Egon B¨orger's 65th birthday. The ABZ proceedings appear as a separate LNCS volume, number 7316. The invited talk of Egon B¨orger appears in both proceedings. The iFM conference programme also included an invited talk by Muffy Calder and the ABZ conference programme included an invited talk by Ian Hayes. Previous iFM conferences were held in York, Dagstuhl, Turku, Canterbury, Eindhoven, Oxford, D¨usserldorf and Nancy. The iFM conference series seeks to further research into the combination of different formal methods for modelling and analysis. However, the work of iFM goes beyond that, covering all aspects from language design, verification techniques, tools and the integration of formal methods into software engineering practice. iFM 2012 received 59 submissions, covering the spectrum of integrated formal methods, ranging across formal and semi-formal modelling notations, semantics, proof frameworks, refinement, verification, timed systems, tools and case studies. Each submission was reviewed by at least three Programme Committee members. The committee decided to accept 22 papers. The conference was preceded by a day dedicated to tutorials on "Practical Predicative Programming Primer" by Eric C. R. Hehner and "Safety, Dependability and Performance Analysis of Extended AADL Models" by Joost-Pieter Katoen, Thomas Noll, Alessandro Cimatti and Marco Bozzano. We are grateful to the members of the Programme Committee and the external reviewers for their diligence and thoroughness. We also appreciate the support of EasyChair for managing the reviewing process and the preparation of the proceedings. We thank all those involved in organizing the conference and an important note of thanks must be extended to the members of CNR who helped locally. June