Accepted Papers

• Pointer Program Derivation using Coq: Graphs and Schorr-Waite Algorithm
  Jean-François Dufourd
• Extending MSVL with Function Calls
  Nan Zhang, Zhenhua Duan and Cong Tian
• Fast Translation from LTL to Büchi Automata via Non-Transition-based Automata
  Shohei Mochizuki, Masaya Shimakawa, Shigeki Hagihara and Naoki Yonezaki
• GPU Accelerated Dynamic Counterexample Generation in LTL Model Checking
  Zhimin Wu, Yang Liu, Yun Liang and Jun Sun
• Practical Analysis Framework for Software-based Attestation Scheme
  Li Li, Hong Hu, Jun Sun, Yang Liu and Jin Song Dong
• TAuth: Verifying Timed Security Protocols
  Li Li, Jun Sun, Yang Liu and Jin Song Dong
• Bounded Model Checking High Level Petri Nets in PIPE+Verifier
  Su Liu, Reng Zeng, Zhuo Sun and Xudong He
• GRL: a Specification Language for Globally Asynchronous Locally Synchronous Systems
  Fatma Jebali, Frederic Lang and Radu Mateescu
• Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints
  Simon Busard, Charles Pecheur, Hongyang Qu and Franco Raimondi
• SCC-based Improved Reachability Analysis for Markov Decision Processes
  Lin Gui, Jun Sun, Songzheng Song, Yang Liu and Jin Song Dong
• Formal Modeling and Analysis of Cassandra in Maude
  Si Liu, Muntasir Raihan Rahman, Stephen Skeirik, Indranil Gupta and Jose Meseguer
• A Formula-based Approach for Automatic Fault Localization of Imperative Programs
  Si-Mohamed Lamraoui and Shin Nakajima
• Timed Automata Verification via IC3 with Zones
  Tobias Isenberg and Heike Wehrheim
• CASSANDRA an Online Failure Prediction Strategy for Dynamically Evolving Systems
  Francesco De Angelis, Andrea Polini, Henry Muccini and Maria Rita Di Berardini
• Computing Maximal Bisimulations of Labelled Transition Systems
  Alexandre Boulgakov, Thomas Gibson-Robinson and A. W. Roscoe
• Modal Characterisations of Probabilistic and Fuzzy Bisimulations
  Yuxin Deng and Hengyang Wu
• Formal Throughput and Response Time Analysis of MARTE Models
  Gaogao Yan, Xue-Yang Zhu, Rongjie Yan and Guangyuan Li
• A Language-Independent Proof System for Mutual Program Equivalence
  Stefan Ciobaca, Dorel Lucanu, Vlad Rusu and Grigore Rosu
• A Resource-Based Logic for Termination and Non-Termination Proofs
  Ton Chanh Le, Cristian Gherghina, Aquinas Hobor and Wei-Ngan Chin
• A Hybrid Model of Connectors in Cyber-Physical Systems
  Xiaohong Chen, Jun Sun and Meng Sun
• Contract-based Verification of MATLAB and Simulink Matrix-manipulating Code
  Jonatan Wiik and Pontus Boström
• An LTL Model Checking Approach for Biological Parameter Inference
  Emmanuelle Gallet, Matthieu Manceny, Pascale Le Gall and Paolo Ballarini
• PHASE: A Stochastic Formalism for Phase-Type Distributions
  Gabriel Ciobanu and Armand Stefan Rotaru
• 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
• A Formal Model for Analysing Natural Language Timed Requirements of Reactive Systems
  Gustavo Carvalho, Ana Carvalho, Eduardo Rocha, Augusto Sampaio and Ana Cavalcanti
• Comprehension of Spacecraft Telemetry using Hierarchical Specifications of Behavior
  Klaus Havelund and Rajeev Joshi
• On the Formal Analysis of HMM using Theorem Proving
  Liya Liu, Osman Hasan and Sofiene Tahar
• A Formal Framework to Prove the Correctness of Model Driven Engineering Composition Operators
  Mounira Kezadri, Marc Pantel, Benoit Combemale and Xavier Thirioux