FMICS 2015 Program

Program

Monday, June 22nd

Time Presentation
End of Day One
9:00 - 10:00 Invited Talk: Formal Verification of Industrial Critical Software Marielle Petit-Doche (Systerel)
10:00 - 10:30 coffee break
Session Applications
10:30 - 11:00 A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre and Frédéric Loulergue
11:00 - 11:30 Intra-Procedural Optimization of the Numerical Accuracy of Programs Nasrine Damouche, Matthieu Martel and Alexandre Chapoutot
11:30 - 12:00 Successful Use of Incremental BMC in the Automotive Industry Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige and Tom Bienmüller
12:00 - 12:30 Formal Analysis and Testing of Real-time Automotive Systems using UPPAAL Tools Jin Hyun Kim, Kim G. Larsen, Petur Olsen, Brian Nielsen and Marius Mikucionis
12:30 - 14:00 lunch
14:00 - 15:00 Invited Talk: From Timed Automata to Stochastic Hybrid Games Kim G. Larsen (Aalborg University)
15:00 - 15:30 Time for Discussions etc.
15:30 - 16:00 coffee break
Session Protocols
16:00 - 16:30 Colored Petri Net Modeling of the Publish/Subscribe Paradigm in the Context of Web Services Resources Valentin Valero, Hermenegilda Macia, Gregorio Díaz and M. Emilia Cambronero
16:30 - 17:00 Modeling and Verification for the Server-Side Netpay Protocol Kaylash Chaudhary and Ansgar Fehnker

Tuesday, June 23rd

Time Presentation
End of Day Two
9:00 - 10:00 Invited Talk: Formal Patterns for Web and Cloud Computing (shared with WWV 2015) José Meseguer (University of Illinois at Urbana-Champaign, USA)
10:00 - 10:30 coffee break
Session Specification and Analysis
10:30 - 11:00 Require, Test and Trace IT Bernhard K. Aichernig, Klaus Hörmaier, Florian Lorber, Dejan Nickovic and Stefan Tiran
11:00 - 11:30 Applying Finite State Process Algebra to Formally Specify a Computational Model of Security Requirements in the Key2phone-Mobile Access Solution Sunil Chaudhary, Linfeng Li, Eleni Berki, Marko Helenius, Juha Kela and Markku Turunen
11:30 - 12:00 Timed Mobility and Timed Communication for Critical Systems Bogdan Aman and Gabriel Ciobanu
12:00 - 12:30 On the Formal Analysis of Photonic Signal Processing Systems Umair Siddique, Sidi Mohamed Beillahi and Sofiene Tahar
12:30 - 14:00 lunch
14:00 - 15:00 Invited Talk: Moving fast with software verification (shared with WWV 2015) Dino Distefano (Queen Mary University, London, UK & Facebook)
15:00 - 15:30 Time for Discussions etc.
15:30 - 16:00 coffee break
Session Verification
16:00 - 16:30 Automated Verification of Nested DFS Jaco van de Pol
16:30 - 17:00 On the Formal Verification of Optical Quantum Gates in HOL Mohamed Yousri Mahmoud, Prakash Panangaden and Sofiene Tahar