CALL FOR PARTICIPATION *********************************************************************************************************************************** 11th International Conference on integrated Formal Methods, iFM 2014 Co-located with the 11th International Symposium on Formal Aspects of Component Software, FACS 2014 9 - 12 September 2014, Bertinoro, Italy http://ifm2014.cs.unibo.it *********************************************************************************************************************************** Applying formal methods may involve modeling different aspects of a system which are best expressed using different formalisms. Correspondingly, different analysis techniques may be used to examine different system views, different kinds of properties, or simply in order to cope with the sheer complexity of the system. The iFM conference series seeks to further research into hybrid approaches to formal modeling and analysis; i.e., the combination of (formal and semi-formal) methods for system development, regarding modeling and analysis, and covering all aspects from language design through verification and analysis techniques to tools and their integration into software engineering practice. CONFERENCE LOCATION iFM 2014 is organized by the University of Bologna and will take place at the Centro Residenziale Universitario in Bertinoro, a small medieval hilltop town 50 km east of Bologna. The conference program includes a visit of “Rocca” with a welcome cocktail on Tuesday, 9 September and a visit of “Fattoria Paradiso" with social dinner on Wednesday, 10 September. REGISTRATION Registration to the conference and workshops, as well as hotel reservation, is directly managed by the Centro Residenziale Universitario in Bertinoro, see: http://ifm2014.cs.unibo.it/registration.html INVITED SPEAKERS iFM 2014 has the following keynote speakers jointly with FACS 2014: Sophia Drossopoulou (Imperial College): Towards Capability Policy Specification and Verification Rocco De Nicola (IMT Lucca): A formal approach to autonomic systems programming: The SCEL Language Helmut Veith (TU Wien): Shape and Content: A database-theoretic perspective on the analysis of data structures Jean-Bernard Stefani (INRIA): TBA PROGRAM Tool Integration: Marcel Vinicius Medeiros Oliveira, Augusto Sampaio and Madiel Conserva. Model-checking Circus State-Rich Specifications Martin Hentschel, Stefan Käsdorf, Reiner Hähnle and Richard Bubel. An interactive verification tool meets an IDE Andrea Vandin, Mirco Tribastone and Stephen Gilmore. An Analysis Pathway for the Quantitative Evaluation of Public Transport Systems Messaoud Abbas, Choukri-Bey Ben-Yelles and Renaud Rioboo. Modeling UML template classes with FoCaLiZe Linas Laibinis, Benjamin Byholm, Inna Pereverzeva, Elena Troubitsyna, Kuan Eeik Tan and Ivan Porres. Integrating Event-B Modelling and Discrete Event Simulation to Analyse Resilience of Data Stores in the Cloud Asieh Salehi Fathabadi, Colin Snook and Michael Butler. Applying an Integrated Modelling Process to Run-time Management of Many-Core Systems Model Verification: Yael Meller, Orna Grumberg and Karen Yorav. Verifying Behavioral UML Systems via CEGAR Alvaro Miyazawa and Ana Cavalcanti. Formal refinement in SysML Hadrien Bride, Olga Kouchnarenko and Fabien Peureux. Verifying Modal Workflow Specifications using Constraint Solving Program Development: Johannes Eriksson, Masoumeh Parsa and Ralph-Johan Back. Proofs and Refutations in Invariant-Based Programming Dipak L. Chaudhari and Om Damani. Automated Theorem Prover Assisted Program Calculations Steve Schneider, Helen Treharne, Heike Wehrheim and David M. Williams. Managing LTL properties in Event-B refinement Security Analysis: Alessandro Bruni, Michal Sojka, Flemming Nielson and Hanne Riis Nielson. Formal and Experimental Security Analysis of the MaCAN Protocol Barbara Kordy, Patrick Schweitzer and Marc Pouly. A Probabilistic Framework for Security Scenarios with Dependent Actions John Ramsdell, Daniel Dougherty, Joshua Guttman and Paul Rowe. A Hybrid Analysis for Security Protocols with State Analysis and Transformation: Irina Mariuca Asavoae, Mihail Asavoae and Adrian Riesco. Towards a Formal Semantics-Based Technique for Interprocedural Slicing Marie-Christine Jakobs, Marco Platzner, Heike Wehrheim and Tobias Wiersema. Integrating Software and Hardware Verification Andreas Fürst, Thai Son Hoang, David Basin, Krishnaji Desai, Naoto Sato and Kunihiko Miyazaki. Code Generation for Event-B Concurrency and Control: John Derrick, Graeme Smith and Brijesh Dongol. Verifying Linearizability on TSO Architectures Bogdan Tofan, Gerhard Schellhorn and Wolfgang Reif. A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset Lucian Patcas, Mark Lawford and Tom Maibaum. A Separation Principle for Embedded System Interfacing WORKSHOPS Harnessing Theories for Tool Support in Software (TTSS), 9 September 2014: http://facs2014.cs.unibo.it/TTSS Volker Stolz, University of Oslo, Norway (Organizer) Michael Lienhardt, University of Bologna, Italy (Organizer) Logics and Model-checking for Self-* Systems (MOD*),12 September 2014: http://modstar.cs.unibo.it Marcello M. Bersani, Politecnico di Milano, Italy (Organizer) Davide Bresolin, University of Bologna, Italy (Organizer) Luca Ferrucci, Politecnico di Milano, Italy (Organizer) Manuel Mazzara, Politecnico di Milano, Italy (Organizer) Tools and Methods for Cyber-Physical Systems of Systems,12 September 2014: http://www.cpsos.eu John Fitzgerald, Newcastle University, UK (Organizer) Wan Fokkink, VU University Amsterdam, The Netherlands (Organizer) Michel Reniers, Technical University Eindhoven, The Netherlands (Organizer) Workshop on Contracts for Efficient and Reliable Services, 12 September 2014 http://facs2014.cs.unibo.it/EC-SLA Mario Bravetti, University of Bologna/INRIA, Italy (Organizer) Elena Giachino, University of Bologna/INRIA, Italy (Organizer) Formal Methods: Business Impact of Application to Security relevant Devices (FM-BIASED), 9 September 2014: http://www.fm-biased.eu Beatrice Albè, Novareckon S.R.L., Italy (Organizer) Alberto Stefanini, Novareckon S.R.L., Italy (Organizer) GENERAL CHAIR Gianluigi Zavattaro, University of Bologna, Italy iFM PROGRAMME COMMITTEE CHAIRS: Elvira Albert, Complutense University of Madrid, Spain Emil Sekerinski, McMaster University, Canada FMCO and iFM WORKSHOP CHAIR Elena Giachino, University of Bologna, Italy iFM PROGRAM COMMITTEE Erika Abraham, RWTH Aachen University, Germany Clara Benac, Technical University of Madrid, Spain Ana Cavalcanti, University of York, UK Frank de Boer, CWI Amsterdam, Netherlands Eerke Boiten, University of Kent, UK Michael Butler, University of Southampton, UK David Déharbe, Federal University of Rio Grande do Norte, Brazil John Derrick, University of Sheffield, UK Marc Frappier, University of Sherbrooke, Canada Elena Giachino, University of Bologna, Italy Susanne Graf, Verimag, France John Hatcliff, Kansas State University, USA Einar Broch Johnsen, University of Oslo, Norway Rajeev Joshi, NASA Jet Propulsion Laboratory, USA Laura Kovács, Chalmers University of Technology, Sweden Diego Latella, National Research Council, Pisa, Italy Stefan Leue, University of Konstanz, Germany Shaoying Liu, Hosei University, Japan Dominique Mery, LORIA and University of Lorraine, France Antoine Mine, Ecole Normale Supérieur, France Luigia Petre, Åbo Akademi University, Finland Guillermo Román Díez, Technical University of Madrid, Spain Fernando Rosa, Complutense University of Madrid, Spain Augusto Sampaio, University of Pernambuco, Brazil Thomas Santen, European Microsoft Innovation Center, Germany Steve Schneider, University of Surrey, UK Graeme Smith, University of Queensland, Australia Kenji Taguchi, AIST, Japan Tayssir Touili, University Paris Diderot, France Helen Treharne, University of Surrey, UK Jüri Vain, Tallinn University of Technology, Estonia Heike Wehrheim, University of Paderborn, Germany Peter Wong, Fredhopper B.V., Netherlands