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.

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 Speciļ¬cations 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
FNR Logo CSC Logo