[TYPES/announce] FM 2015, Oslo: 2nd call for participation: Early registration ends 20 May!

[Martin Steffen]

-----------------------------------------------------------------
       !!!      IMPORTANT: early registration ends soon  !!!
              Early registration deadline: May 20, 2015  
----------------------------------------------------..............
--------===           FM 2015           ===-----

              Second   Call for Participation
	     
       20th International Symposium on Formal Methods

               Oslo, Norway, June 22-26, 2015
 
                     http://fm2015.ifi.uio.no/

-----------------------------------------------------------------------


This year's International Symposium on Formal Methods, FM2015, 
will be held June 22-26 (which includes the year's longest(!) and
hopefully sunniest days in Oslo).


o ABOUT FM (International Symposium on Formal Methods)

 FM 2015 is the twentieth in a series of symposia organized by Formal
 Methods Europe, an independent association whose aim is to stimulate the
 use of, and research on, formal methods for software development.  The
 symposia have been notably successful in bringing together innovators and
 practitioners in precise mathematical methods for software and systems
 development, industrial users, as well as researchers.


o CONFERENCE AND SATELLITE EVENTS:

Satellite events:                22-23 June, 2015 (Mon - Tue) 
FM2015 Main conference:          24-26 June, 2015 (Wed - Fri)


o FM 2015 KEYNOTE SPEAKERS

   Elvira Albert, Complutense University of Madrid, ES
   Werner Damm, Carl von Ossietzky Universitaet Oldenburg, DE
   Valerie Issarny, INRIA, FR
   Leslie Lamport, Microsoft Research, US

o FME FELLOWSHIP AWARD

o WORKSHOPS

- FMICS (22-23th June)
   Keynote: Kim G. Larsen, Aalborg University, DK
   Keynote: Marielle Petit-Doche, Systerel, FR

- Overture/VDM (23 June)
   Keynote: Taro Kurita, Sony Corporation, JP

- WWV: Automated Specification and Verification of Web systems (23 June)
   Keynote: Dino Distefano, Queen Mary University & Facebook, UK
   Keynote: José Meseguer, University of Illinois, US

- Refinement (22 June)
- ESSS: Engineering Safety and Security Systems (22 June)
   Keynote: Marieke Huisman, University of Twente, NL
   Keynote: Audun Jøsang, University of Oslo, NO

- USE: Usages of Symbolic Execution (23 June) 
- SETS: Sets and Tools (23 June)
- FMSEET: Formal Methods in Software Education and Training (23 June)
- F-IDE: Formal Integrated Development Environments (22 June)

o  DOCTORAL SYMPOSIUM (22 June) 
   Keynote: Stijn de Gouw, SDL, NL

o  TUTORIALS

- Modelling and Analysis of Communicating Systems
   Jan Friso Groote (Eindhoven University of Technology, NL),
   Mohammad Mousavi (Halmstad University, SE),
   Tim Willemse (Eindhoven University of Technology, NL)
	
- The Correctness-by-Construction Approach to Programming
   Bruce Watson (FASTAR research group, ZA)
   Derrick Kourie (FASTAR research group, ZA)
   Loek Cleophas (FASTAR research group, ZA, and Umeå University, SE)

- Abstract Behavioral Specification
   Reiner Hähnle (Technische Universität Darmstadt, DE),
   Einar Broch Johnsen (University of Oslo, NO)

- Theory and Practice of Runtime Verification
   Martin Leucker (Universität zu Lübeck, DE)
   Daniel Thoma (Universität zu Lübeck, DE)

 o FM2015 ACCEPTED PAPERS MAIN CONFERENCE

- Cornelius Diekmann, Lars Hupel and Georg Carle.
   Semantics-Preserving Simplification of Real-World Firewall Rule Sets

-Nadia Polikarpova, Julian Tschannen and Carlo A. Furia.
  A Fully Verified Container Library

- Alexey Solovyev, Charlie Jacobsen, Zvonimir Rakamaric and Ganesh Gopalakrishnan.
   Rigorous Estimation of Floating-Point Round-off Errors with Symbolic

- Taylor Expansions Shin Nakajima.
   Using Real-Time Maude to Model Check Energy Consumption Behavior

- Li Li, Jun Sun, Yang Liu and Jin Song Dong.
   Verifying Parameterized Timed Security Protocols

- Jiang Liu, Naijun Zhan, Hengjun Zhao and Liang Zou.
   Abstraction of Elementary Hybrid Systems by Variable Transformation

- Tommaso Dreossi, Thao Dang and Carla Piazza.
   Parameter Synthesis through Temporal Logic Specifications

- Peter Schmitt and Mattias Ulbrich.
   Typed First-Order Logic

- Jesus Mauricio Chimento, Wolfgang Ahrendt, Gerardo Schneider and Gordon Pace.
   A Specification Language for Static and Runtime Verification of Data and Control Properties

- Karam Abdelkader, Orna Grumberg, Corina Pasareanu and Sharon Shoham.
   Automated Circular Assume-Guarantee Reasoning

- Xue-Yang Zhu, Rongjie Yan, Yu-Lei Gu, Jian Zhang, Wenhui Zhang and Guangquan Zhang.
   Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking

- Tim Nelson, Andrew D. Ferguson and Shriram Krishnamurthi.
   Static Differential Program Analysis for Software-Defined Networks

- Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz.
   Automated Verification of RPC Stub Code

- Yuan Feng, Ernst Moritz Hahn, Andrea Turrini and Lijun Zhang.
   QPMC: A Model Checker for Quantum Programs and Protocols

- Julien Bringer, Hervé Chabanne, Daniel Le Métayer and Roch Lescuyer.
   Privacy by design in practice: reasoning about privacy properties
   of biometric system architectures

- Musab A. Alturki and Omar Alzuhaibi.
   Towards Formal Verification of Orchestration Computations Using the K Framework

- Christian Eisentraut, Jens Chr. Godskesen, Holger Hermanns, Lei Song and Lijun Zhang.
   Probabilistic Bisimulation for Realistic Schedulers

- Temesghen Kahsai, Falk Howar, Dimitra Giannakopoulou, Guillaume Brat and Misty Davies.
   Verifying the Safety of a Flight-Critical System

- Gianluca Amato, Simone Di Nardo Di Maio, Maria Chiara Meo and Francesca Scozzari.
   Narrowing operators on template abstract domains

- Xiaoning Du, Yang Liu and Alwen Tiu.
   Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL

- David Schneider, Michael Leuschel and Tobias Witt.
   Model-Based Problem Solving for University Timetable Validation and Improvement

- Søren Debois, Thomas Hildebrandt and Tijs Slaats.
   Safety, Liveness and Run-time Refinement for Modular Process-Aware
   Information Systems with Dynamic Sub Processes

- Saurabh Joshi and Daniel Kroening.
   Property-Driven Fence Insertion using Reorder Bounded Model Checking

- Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika
   Abraham, Joost-Pieter Katoen and Bernd Becker.
   Counterexamples for Expected Rewards

- Daniel Kroening, Matt Lewis  and Georg Weissenbacher.
   Proving Safety with Trace Automata and Bounded Model Checking

- John Derrick and Graeme Smith.
   A framework for correctness criteria on weak memory models

- John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin
   and Heike Wehrheim.
   Verifying Opacity of a Transactional Mutex Lock

- Aliakbar Safilian, Tom Maibaum and Zinovy Diskin.
   The Semantics of Cardinality-based Feature Models via Formal Languages

- Sylvain Conchon, Alain Mebsout and Fatiha Zaidi.
   Certificates for Parameterized Model Checking

- Hamid Bagheri, Eunsuk Kang, Sam Malek and Daniel Jackson.
   Detection of Design Flaws in the Android Permission Protocol
   through Bounded Verification

-  Andrew Sogokon and Paul Jackson.
    Direct formal verification of liveness properties in continuous and
    hybrid dynamical systems

- Asankhaya Sharma, Shengyi Wang, Andreea Costea, Aquinas Hobor and Wei-Ngan Chin.
   Certified Reasoning with Infinity


 o FM2015 ACCEPTED PAPERS INDUSTRY TRACK

- Rodrigo Reis, Henrique Masini and Bruno Miranda.
   Using Simulink Design Verifier for automatic generation of
   requirements-based testing

- Ralf Huuck and Tao Liu.
   Case Study: Static Security Analysis of the Android Goldfish Kernel

- Stefan Hauck-Stattelmann, Sebastian Biallas, Bastian Schlich,
   Stefan Kowalewski and Raoul Jetley.
   Analyzing the Restart Behavior of Industrial Control Applications

- Bharti Chimdyalwar, Priyanka Darke, Anooj Chavda, Sagar Vaghani and Avriti Chauhan.
   Eliminating static analysis false positives using loop abstraction
   and bounded model checking

- Mathijs Schuts and Jozef Hooman.
   Formalizing the Concept Phase of Product Development at Philips Healthcare

- Neil Evans.
   Software Development and Authentication for Arms Control Information Barriers

- William Durand and Sébastien Salva.
   Autofunk: an inference-based formal model generation framework for
   production systems.

- Taro Kurita, Fuyuki Ishikawa and Keijiro Araki.
   Practices for Formal Models as Documents: Evolution of VDM
   Application to "Mobile FeliCa" IC Chip Firmware

- Thierry Lecomte.
   Formal Virtual Modelling and Data Verification for Supervision Systems