Session 1: Transition systems and bisimulations

• Sebastian Küpper, Barbara König, Alexandra Silva and Harsh Beohar. Conditional Transition Systems with Upgrades
• Yuxin Deng and Yuan Feng. Bisimulations for Probabilistic Lambda Calculi
• Tian-Ming Bu, Hengyang Wu and Yixiang Chen. Computing Behavioural Distance for Fuzzy Transition System

Session 2: SAT/SMT, algorithms and applications

• Yueling Zhang, Jianwen Li, Min Zhang, Geguang Pu and Fu Song. Optimizing Backbone Filtering
• Juliana Küster Filipe Bowles, Marco B. Caminati and Suhyun Cha. An Integrated Framework for Verifying Multiple Care Pathways
• Pattaravut Maleehuan, Yuki Chiba and Toshiaki Aoki. Assembly Program Verification for Multiprocessors with Relaxed Memory Model using SMT Solver

Session 3: Real-time and event systems

• Ning Ge, Marc Pantel and Silvano Dal Zilio. Formal Verification of User-Level Real-Time Property Patterns
• Chunyan Mu and Shengchao Qin. Time-sensitive Information Flow Control in Timed Event-B
• Jacques Julliand, Olga Kouchnarenko, Pierre-Alain Masson and Guillaume Voiron. Two Under-Approximation Techniques for 3-Modal Abstraction Coverage of Event Systems: Joint Effort?

Session 4: Program analysis and testing

• Haiyang Liu, Tingting Hu and Zongyan Qiu. Automatic Fine-grain Locking Generation for Shared Data Structures
• Zeineb Zhioua, Yves Roudier and Rabea Boulifa Ameur. Formal Specification of Security Guidelines for Program Certification
• Claudio Antares Mezzina and Vasileios Koutavas. A Safety and Liveness Theory for Total Reversibility

Session 5: System modeling

• Ning Ge, Arnaud Dieumegard, Eric Jenn, Bruno D’ausbourg and Yamine Aït-Ameur. Formal Development Process of Safety-Critical Embedded Human Machine Interface Systems
• Bingqing Xu and Qin Li. A Bounded Multi-dimensional Modal Logic for Autonomous Cars Based on Local Traffic and Estimation
• Diego Marmsoler. On the Semantics of Temporal Specifications of Component-Behavior for Dynamic Architectures
• Shichao Liu and Ying Jiang. Modeling and Reasoning About Wireless Networks: A Graph-based Calculus Approach

Session 6: Verification and visualization

• Yan Ma, Zining Cao and Yang Liu. PSO-based refinement for CEGAR in stochastic model checking
• Messaoud Rahim, Malika Ioualalen and Ahmed Hammad. Slicing Based Verification Approach for the Validation of SysML Activity Diagrams
• Jian Liu, Ying Jiang and Yanyun Chen. VMDV: A 3D Visualization Tool for Modeling, Demonstration, and Verification