[Air-L] FM 2016: 21st International Symposium on Formal Methods -- Call for Participation

[Announce Announcements]

----------------------------------------------------------------------------------
**** CALL FOR PARTICIPATION ****
FM 2016: 21st International Symposium on Formal Methods
Limassol, Cyprus, 7-11 November 2016
fm2016.cs.ucy.ac.cy
Early Registration Deadline: 6 October 2016
----------------------------------------------------------------------------------

FM 2016, the 21st International Symposium on research and practice in Formal Methods, will be held this year on the ancient and beautiful Mediterranean island of Cyprus. Every 18 months, the FM symposium attracts practitioners and researchers from industry and academia to present and discuss the most recent results and experience in formal methods. Those who join us in Cyprus this year will enjoy a highly selective programme of papers covering the broad range of formal methods, as well as a featured track on industry practice. Workshops will provide an opportunity to work in smaller groups on current challenges; tutorials will allow the acquisition of new skills; and a doctoral symposium will offer advice and encouragement to researchers just beginning their careers in this exciting and rapidly evolving field.
The conference will take place in Limassol, Cyprus.  Limassol is the second largest city in Cyprus. It is located on the south coast of the island, between the ancient towns of Amathus and Kourion. Limassol is renowned for its extensive cultural traditions, and it offers a wide spectrum of activities and a number of museums and archaeological sites to the interested visitor. Indeed, this richly cultured, cosmopolitan, seaside city has become one of the most important tourism destinations in Cyprus. The venue of the summer school will be the 5-star St. Raphael Resort, located on one of the most renowned and largest beaches, only a short coastal drive from the lively centre of Limassol.

REGISTRATION
You can register at the FM 2016 website:  http://www.cs.ucy.ac.cy/~george/lm/lm.php?tk=YWlyLUwJCQlhaXItTEBsaXN0c2Vydi5hb2lyLm9yZwlGTSAyMDE2OiAyMXN0IEludGVybmF0aW9uYWwgU3ltcG9zaXVtIG9uIEZvcm1hbCBNZXRob2RzIC0tIENhbGwgZm9yIFBhcnRpY2lwYXRpb24JNjUJTGlzdHMJMjQ3CWNsaWNrCXllcwlubw==&url=http%3A%2F%2Ffm2016.cs.ucy.ac.cy%2Fregistration.html

HIGHLIGHTS
-	44 regular papers and ten short papers reflecting the current state of research and practice in formal methods, including a track on industry practice
-	Three world-class keynote speakers
-	A Doctoral Symposium, six specialist workshops and eight tutorials
-	Presentation of the first FME Lucas Award for a Highly Influential Publication
-	Launch of Springer's new LNCS Formal Methods subline

KEYNOTE SPEAKERS
-	Manfred Broy, Technical University of Munich, Germany
-	Peter O'Hearn, University College London and Facebook, UK
-	Jan Peleska, University of Bremen and Verified Software International, Germany

WORKSHOPS (http://fm2016.cs.ucy.ac.cy/workshops.html)
-	ESSS 2016: 5th International Workshop on Engineering Safety and Security Systems
-	F-IDE 2016: 3rd Workshop on Formal Integrated Development Environment
-	FM-Priv 2016: 1st Workshop on Formal Methods for Privacy
-	Overture 2016: 14th Overture Workshop
-	TLA+ 2016: International Workshop on the TLA+ Method and Tools
-	USE 2016: 2nd Workshop on Usages of Constraint Solving and Symbolic Execution

DOCTORAL SYMPOSIUM (http://fm2016.cs.ucy.ac.cy/cfpdoctoralsymposium.html)
This symposium aims to provide a helpful environment in which selected PhD students can present and discuss their ongoing work, meet other students working on similar topics, and receive helpful advice and feedback from a panel of researchers and academics.
-	Keynote Speaker: John S. Fitzgerald, Newcastle University, UK

TUTORIALS (http://fm2016.cs.ucy.ac.cy/tutorials.html )
-	Abstraction and Rely/Guarantee Thinking
Tutors: Cliff Jones, Newcastle University, UK; Ian Hayes, University of Queensland, AU
-	Compositional Verification using AADL and the Assume Guarantee Reasoning Environment (AGREE)
Tutor: Michael Whalen, University of Minnesota, USA
-	Cyber-Physical Systems Engineering: Next Generation Foundations, Methods and Tools
Tutors: John Fitzgerald, Newcastle University, UK; Peter Gorm Larsen, Aarhus University, DK; Jim Woodcock, University of York, UK; Ken Pierce, Newcastle University, UK; Simon Foster, University of York, UK
-	First-Order Theorem Proving and Vampire
Tutors: Laura Kovacs, Chalmers University of Technology, SE; Andrei Voronkov, University of Manchester, UK
-	KeYmaera X Tutorial - Tactics and Proofs for Cyber-Physical Systems
Tutors: Stefan Mitsch, Carnegie Mellon University, USA; Nathan Fulton, Carnegie Mellon University, USA; André Platzer, Carnegie Mellon University, USA
-	Modelling and Analysis of Collective Adaptive Systems
Tutors: Jane Hillston, University of Edinburgh, UK; Michele Loreti, Università di Firenze, IT
-	Session Types for Concurrent and Distributed Programming: Principles and Practice
Tutors: Raymond Hu, Imperial College London, UK; Jorge A. Pérez, University of Groningen, NL; Nobuko Yoshida, Imperial College London, UK
-	The CProver Suite of Verication Tools
Tutors: Daniel Kroening, University of Oxford, UK; Martin Brain, University of Oxford, UK; Peter Schrammel, University of Sussex, UK

ACCEPTED PAPERS (Research Track)
Li Li, Jun Sun and Jin Song Dong. Automated Verification of Timed Security Protocols with Clock Drift
Victor B. F. Gomes and Georg Struth. Modal Kleene Algebra Applied to Program Correctness
Artem Khyzha, Alexey Gotsman and Matthew Parkinson. A Generic Logic for Proving Linearizability
Antonio E. Flores Montoya. Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations
Ian J. Hayes, Robert Colvin, Larissa Meinicke, Kirsten Winter and Andrius Velykis. An algebra of synchronous atomic steps
Zhe Hou, David Sanan, Alwen Tiu, Yang Liu and Koh Chuen Hoa. An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor
Nikola Benes, Lubos Brim, Martin Demko, Samuel Pastva and David ?afránek. A Model Checking Approach to Discrete Bifurcation Analysis
Mahieddine Dellabani, Saddek Bensalem, Jacques Combaz and Marius Bozga. Local Planning of Multiparty Interactions with a Bounded Horizon
Adel Djoudi, Sébastien Bardin and Éric Goubault. Recovering high-level conditions from binary programs
Thomas Letan, Pierre Chifflier, Guillaume Hiet, Benjamin Morin and Ludovic Mé. SpecCert: Verifying Hardware-based Security Enforcement
Hanno Becker, Juan Manuel Crespo, Jacek Galowicz, Ulrich Hensel, Yoichi Hirai, César Kunz, Keiko Nakata, Jorge Luis Sacchini, Hendrik Tews and Thomas Tuerk. Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
Dimitra Giannakopoulou, Dennis Guck and Johann Schumann. Exploring Model Quality for ACAS X
Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening and Tom Melham. Equivalence Checking of a Floating-point Unit Against a High-level C Model
Yusuke Kawamoto, Fabrizio Biondi and Axel Legay. Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow
Bat-Chen Rothenberg and Orna Grumberg. Sound and Complete Mutation-Based Program Repair
Miran Hasanagic, Peter Gorm Larsen, Peter W. V. Tran-Jørgensen and Kenneth Lausdahl. Formalising and Validating the Interface Description in the FMI standard
Zhengfeng Yang, Chao Huang, Xin Chen, Wang Lin and Zhiming Liu. A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems
Ofer Strichman and Maor Veitsman. Regression Verification for unbalanced recursive functions
Cristina David, Pascal Kesseli, Daniel Kroening and Matt Lewis. Danger Invariants
Gaogao Yan, Li Jiao, Yangjia Li, Shuling Wang and Naijun Zhan. Approximate Bisimulation and Discretization of Hybrid CSP
Tsutomu Kobayashi, Fuyuki Ishikawa and Shinichi Honiden. Refactoring Refinement Structures of Event-B Machines
Pingfan Kong, Yi Li, Xiaohong Chen, Jun Sun, Meng Sun and Jingyi Wang. Towards Concolic Testing for Hybrid Systems
Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad and Naijun Zhan. Validated Simulation-Based Verification of Delayed Differential Dynamics
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo and Wei-Ngan Chin. Automated Mutual Explicit Induction Proof in Separation Logic
Stanislav Böhm, Ond?ej Meca and Petr Jancar. State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI
Christoph-Simon Senjak and Martin Hofmann. An Implementation of Deflate in Coq
Gudmund Grov, Yuhui Lin and Vytautas Tumas. Mechanised Verification Patterns for Dafny
Heinrich Ody, Martin Fränzle and Michael R. Hansen. Discounted Duration Calculus
Lacramioara Astefanoaei, Saddek Bensalem, Marius Bozga, Chih-Hong Cheng and Harald Ruess. Compositional Parameter Synthesis
Ori Lahav and Viktor Vafeiadis. Explaining Relaxed Memory Models with Program Transformations
Amirhossein Vakili and Nancy Day. Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
Saksham Chand, Annie Liu and Scott Stoller. Formal Verification of Multi-Paxos for Distributed Consensus
Aleksandar S. Dimovski, Claus Brabrand and Andrzej Wasowski. Finding Suitable Variability Abstractions for Family-Based Analysis
Anton Wijs, Thomas Neele and Dragan Bosnacki. GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking
Pedro Antonino, Thomas Gibson-Robinson and Bill Roscoe. Tighter Reachability Criteria for Deadlock-Freedom Analysis
Yuqi Chen, Christopher M. Poskitt and Jun Sun. Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
Gilles Nies, Holger Hermanns, Marvin Stenger, Morten Bisgaard, David Gerhardt and Jan Kr?ál. Battery-Aware Scheduling in Low Orbit: The GomX-3 Case
Alessandro Cimatti, Sergio Mover and Mirko Sessa. From Electrical Switched Networks to Hybrid Automata
Claudio Menghi, Paola Spoletini and Carlo Ghezzi. Dealing with Incompleteness in Automata-based Model Checking
Parosh Aziz Abdulla, Mohamed Faouzi Atig and Bui Phi Diep. Counter-Example Guided Program Verification
Andrew Sogokon, Khalil Ghorbal and Taylor T Johnson. Decoupled simulating abstractions of non-linear ordinary differential equations
Georgios Giantamidis and Stavros Tripakis. Learning Moore Machines from Input-Output Traces
Andreas Holzer, Daniel Schwartz-Narbonne, Mitra Tabaei Befrouei, Georg Weissenbacher and Thomas Wies. Error Invariants for Concurrent Traces

ACCEPTED PAPERS (Industry Track - http://www.cs.ucy.ac.cy/~george/lm/lm.php?tk=YWlyLUwJCQlhaXItTEBsaXN0c2Vydi5hb2lyLm9yZwlGTSAyMDE2OiAyMXN0IEludGVybmF0aW9uYWwgU3ltcG9zaXVtIG9uIEZvcm1hbCBNZXRob2RzIC0tIENhbGwgZm9yIFBhcnRpY2lwYXRpb24JNjUJTGlzdHMJMjQ3CWNsaWNrCXllcwlubw==&url=http%3A%2F%2Ffm2016.cs.ucy.ac.cy%2Fcfpindustrytrack.html%29
Teodor Stoenescu, Alin Stefanescu, Sorina Predut and Florentin Ipate. RIVER: A Binary Analysis Framework using Symbolic Execution and Reversible x86 Instructions
Roberto Cavada, Alessandro Cimatti, Luigi Crema, Mattia Roccabruna and Stefano Tonetta. Model-Based Design of an Energy-System Embedded Controller using Taste
Bjørnar Luteberget, Christian Johansen, Claus Feyling and Martin Steffen. Rule-based Incremental Verification Tools Applied to Railway Designs and Regulations
Han Liu, Yu Jiang, Huafeng Zhang, Ming Gu and Jiaguang Sun. Taming Interrupts For Verifying Industrial Multifunction Vehicle Bus Controllers
Predrag Filipovikj, Nesredin Mahmud, Raluca Marinescu, Cristina Seceleanu, Oscar Ljungkrantz and Henrik Lönn. Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
Yu Jiang, Han Liu, Hui Kong, Houbing Song, Ming Gu, Jiaguang Sun and Lui Sha. Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller