Print

Print


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