Key Dates

March 22, 2014

Workshop/Tutorial Proposals

April 25, 2014

Abstract submission deadline (extended)

May 4, 2014

Paper submission deadline (extended)

June 20, 2014


July 13, 2014

Camera-ready due

Author registration deadline

September 27, 2014

Early registration deadline

November 3-5, 2014

Conference date

November 6-7, 2014

Affiliated workshops date

Recent News

October 14, 2013

The webpage goes live.

Conference Program

Details of the programs of the conference and the workshops (SOFL+MSVL and FTSCS) can be found in one PDF file.

November 3

  • 08:00-08:40 Registration
  • 08:40-08:50 Conference opening (Chair: Sjouke Mauw)
  • 08:50-09:00 Presentation of Fonds National de la Recherche (Carlo Duprel)
  • 09:00-10:00 Keynote talk (Chair: Sjouke Mauw)
    Scalable Software Testing and Verification Through Heuristic Search and Optimization
    Lionel Briand (University of Luxembourg)
  • 10:00-10:30 Coffee break
  • Session 1: Formal Specification (Chair: Pierre Kelsen)

  • 10:30-11:00 Comprehension of Spacecraft Telemetry using Hierarchical Specifications of Behavior
    Klaus Havelund and Rajeev Joshi
  • 11:00-11:30 Extending MSVL with Function Calls
    Nan Zhang and Zhenhua Duan
  • 11:30-12:00 GRL: a Specification Language for Globally Asynchronous Locally Synchronous Systems
    Fatma Jebali, Frederic Lang and Radu Mateescu
  • 12:00-13:30 Lunch break
  • Session 2: Theorem Proving (Chair: José Meseguer )

  • 13:30-14:00 Pointer Program Derivation using Coq: Graphs and Schorr-Waite Algorithm
    Jean-François Dufourd
  • 14:00-14:30 A Formal Framework to Prove the Correctness of Model Driven Engineering Composition Operators
    Mounira Kezadri, Marc Pantel, Benoit Combemale and Xavier Thirioux
  • 14:30-15:00 On the Formal Analysis of HMM using Theorem Proving
    Liya Liu, Osman Hasan and Sofiene Tahar
  • 15:00-15:30 Coffee break
  • Session 3: Safety and Security (Chair: Jun Pang)

  • 15:30-16:00 TAuth: Verifying Timed Security Protocols
    Li Li, Jun Sun, Yang Liu and Jin Song Dong
  • 16:00-16:30 CASSANDRA an Online Failure Prediction Strategy for Dynamically Evolving Systems
    Francesco De Angelis, Andrea Polini, Henry Muccini and Maria Rita Di Berardini
  • 16:30-17:00 Formal Modeling and Analysis of Cassandra in Maude
    Si Liu, Muntasir Raihan Rahman, Stephen Skeirik, Indranil Gupta and Jose Meseguer
  • 17:00-17:30 Practical Analysis Framework for Software-based Attestation Scheme
    Li Li, Hong Hu, Jun Sun, Yang Liu and Jin Song Dong
  • 18:00-20:00 Conference reception

November 4

  • 08:30-09:00 Registration
  • 09:00-10:00 Keynote talk (Chair: Michael Bulter)
    SecGuru: Azure Network Verification using Z3
    Nikolaj Bjorner (Microsoft Research)
  • 10:00-10:30 Coffee break
  • Session 4: Program Analysis (Chair: Shengchao Qin)

  • 10:30-11:00 A Resource-Based Logic for Termination and Non-Termination Proofs
    Ton Chanh Le, Cristian Gherghina, Aquinas Hobor and Wei-Ngan Chin
  • 11:00-11:30 A Formula-based Approach for Automatic Fault Localization of Imperative Programs
    Si-Mohamed Lamraoui and Shin Nakajima
  • 11:30-12:00 Contract-based Verification of MATLAB and Simulink Matrix-manipulating Code
    Jonatan Wiik and Pontus Boström
  • 12:00-13:30 Lunch break
  • Session 5: Model Checking (Chair: Shin Nakajima)

  • 13:30-14:00 An LTL Model Checking Approach for Biological Parameter Inference
    Emmanuelle Gallet, Matthieu Manceny, Pascale Le Gall and Paolo Ballarini
  • 14:00-14:30 SCC-based Improved Reachability Analysis for Markov Decision Processes
    Lin Gui, Jun Sun, Songzheng Song, Yang Liu and Jin Song Dong
  • 14:30-15:00 PHASE: A Stochastic Formalism for Phase-Type Distributions
    Gabriel Ciobanu and Armand Stefan Rotaru
  • 15:00-15:30 Coffee break
  • Session 6: Testing (Chair: Vlad Rusu)

  • 15:30-16:00 A Formal Model for Analysing Natural Language Timed Requirements of Reactive Systems
    Gustavo Carvalho, Ana Carvalho, Eduardo Rocha, Augusto Sampaio and Ana Cavalcanti
  • 16:00-16:30 Complete Model-Based Equivalence Class Testing for the ETCS Ceiling Speed Monitor
    Jan Peleska, Anne E. Haxthausen, Cécile Braunstein, Wen-Ling Huang, Uwe Schulze, Linh Vu Hong and Felix Hübner
  • 16:30-16:45 Break
  • 16:45-17:45 Panel discussion (Chair: Shaoying Liu)
    Are Formal Engineering Methods and Agile Methods Friend or Enemy?
    Panelists: Nikolaj Bjorner, Lionel Briand, Michael Butler, Zhenhua Duan, Shin Nakajima
  • 19:30-22:30 Conference dinner

November 5

  • 08:30-09:00 Registration
  • 09:00-10:00 Keynote talk (Chair: Stephan Merz)
    Approximations for stochastic graph rewriting
    Vincent Danos (University of Edinburgh)
  • 10:00-10:30 Coffee break
  • Session 7: Bisimulation and Program Equivalence (Chair: Jun Sun)

  • 10:30-11:00 Computing Maximal Bisimulations of Labelled Transition Systems
    Alexandre Boulgakov, Thomas Gibson-Robinson and A. W. Roscoe
  • 11:00-11:30 Modal Characterisations of Probabilistic and Fuzzy Bisimulations
    Yuxin Deng and Hengyang Wu
  • 11:30-12:00 A Language-Independent Proof System for Mutual Program Equivalence
    Stefan Ciobaca, Dorel Lucanu, Vlad Rusu and Grigore Rosu
  • 12:00-13:30 Lunch break
  • Session 8: Timed and Hybrid Systems (Chair: Peter Csaba Ölveczky)

  • 13:30-14:00 A Hybrid Model of Connectors in Cyber-Physical Systems
    Xiaohong Chen, Jun Sun and Meng Sun
  • 14:00-14:30 Formal Throughput and Response Time Analysis of MARTE Models
    Gaogao Yan, Xue-Yang Zhu, Rongjie Yan and Guangyuan Li
  • 14:30-15:00 Timed Automata Verification via IC3 with Zones
    Tobias Isenberg and Heike Wehrheim
  • 15:00-15:30 Coffee break
  • Session 9: Model Checking (Chair: Thomas Noll)

  • 15:30-16:00 Bounded Model Checking High Level Petri Nets in PIPE+Verifier
    Su Liu, Reng Zeng, Zhuo Sun and Xudong He
  • 16:00-16:30 Fast Translation from LTL to Büchi Automata via Non-Transition-based Automata
    Shohei Mochizuki, Masaya Shimakawa, Shigeki Hagihara and Naoki Yonezaki
  • 16:30-17:00 GPU Accelerated Dynamic Counterexample Generation in LTL Model Checking
    Zhimin Wu, Yang Liu, Yun Liang and Jun Sun
  • 17:00-17:30 Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints
    Simon Busard, Charles Pecheur, Hongyang Qu and Franco Raimondi
  • 17:30-18:30 Farewell reception

November 6

  • 09:00-17:00 Workshop SOFL+MSVL 2014 (program)
  • 09:10-16:35 Workshop FTSCS 2014 (program)
  • 12:30-17:15 Workshop Default Privacy 2014 (program)

November 7

  • 09:15-15:45 Workshop FTSCS 2014 (program)
  • 09:30-13:45 Workshop Default Privacy 2014 (program)