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
- 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
- 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
- 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
Session 1: Formal Specification (Chair: Pierre Kelsen)
Session 2: Theorem Proving (Chair: José Meseguer )
Session 3: Safety and Security (Chair: Jun Pang)
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
- 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
- 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
- 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
Session 4: Program Analysis (Chair: Shengchao Qin)
Session 5: Model Checking (Chair: Shin Nakajima)
Session 6: Testing (Chair: Vlad Rusu)
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
- 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
- 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
- 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
Session 7: Bisimulation and Program Equivalence (Chair: Jun Sun)
Session 8: Timed and Hybrid Systems (Chair: Peter Csaba Ölveczky)
Session 9: Model Checking (Chair: Thomas Noll)
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)
