Integrated Formal Methods 2014 - 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
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 Kasdorf, Reiner Hahnle 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 Furst, 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:
- 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:
- 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:
- Beatrice Albe, 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 Deharbe, 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 Kovacs, 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 Superieur, France
- Luigia Petre, Abo Akademi University, Finland
- Guillermo Roman Diez, 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
- Juri Vain, Tallinn University of Technology, Estonia
- Heike Wehrheim, University of Paderborn, Germany
- Peter Wong, Fredhopper B.V., Netherlands