CONFERENCE PROGRAM
Day 1: 23 October 2017
08:00–08:30 Registration
08:30–09:00 Welcome by Program Chairs
09:00–10:00 Keynote 1 (Chair: Oleg Sokolsky)
Cliff Jones, Newcastle University
General Lessons from a Rely/Guarantee Development
10:00–10:30 Tea break
10:30–12:00 Session 1 - Probabilistic and statistical analysis (Chair: Lijun Zhang)
10:30–11:00 Vahid Hashemi, Andrea Turrini, Ernst Moritz Hahn, Holger Hermanns and Khaled Elbassioni: Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs
11:00–11:30 Carlos E. Budde, Pedro R. D'Argenio and Arnd Hartmanns: Better Automated Importance Splitting for Transient Rare Events
11:30–12:00 Luca Santinelli and Zhishan Guo: On the Criticality of Probabilistic Worst-Case Execution Time Models
12:15–13:45 Lunch
14:00–15:30 Session 2 – Timed and hybrid systems (Chair: Xiaoguang Mao)
14:00–14:30 Yuwei Wang, Guoqiang Li and Shoji Yuen: Nested Timed Automata with Invariants
14:30–15:00 Calvin Deutschbein, Tom Fleming, Alan Burns and Sanjoy Baruah: Multi-core cyclic executives for safety-critical systems
15:00–15:30 Dimitar Guelev, Shuling Wang and Naijun Zhan: Compositional Hoare-style Reasoning about Hybrid CSP in the Duration Calculus
15:30–16:00 Tea break
16:00–17:30 Session 3 – Program analysis (Chair: Stefano Schivo)
16:00–16:30 Yi Li: Termination of Semi-Algebraic Loop Programs
16:30–17:00 Tianhai Liu, Shmuel Tyszberowicz, Bernhard Beckert and Mana Taghdiri: Computing Exact Loop Bounds for Bounded Program Verification
17:00–17:30 Zipeng Zhang and Xinyu Feng: AndroidLeaker: A Hybrid Checker for Collusive Leak in Android Applications
18:00–19:30 Reception
Day 2：24 October 2017
08:00– 09:00 Registration
09:00–10:00 Keynote 2 (Chair: Naijun Zhan)
Rupak Majumdar, Max Planck Institute for Software Systems
Formal Methods for Building a Multi-Robot Task Server
10:00–10:30 Tea break
10:30–12:00 Session 4 – Modeling and verification I (Chair: Sofiene Tahar)
10:30–11:00 Jianxin Xue, Huan Long and Yuxi Fu: Remark on Some Pi Variants
11:00–11:30 Wanwei Liu, Fu Song and Ge Zhou: Reasoning about Periodicity on Infinite Words
11:30–12:00 Chen Fu, Yuxin Deng, David N. Jansen and Lijun Zhang: On Equivalence Checking of Nondeterministic Finite Automata
12:15–13:45 Lunch
14:00–15:00 Keynote 3 (Chair: Sanjoy Baruah)
Sanjit Seshia, University of California, Berkeley
Towards Verified Artificial Intelligence
15:00–16:00 Session 5 – Formalization (Chair: Zhiping Shi)
15:00–15:30 Ghassen Helali, Sofiene Tahar, Osman Hasan and Tsvetan Dunchev: Formal Analysis of Information Flow in HOL
15:30–16:00 Jiawei Wang, Ming Fu, Lei Qiao and Xinyu Feng: Formalizing SPARCv8 Instruction Set Architecture in Coq
16:00–16:30 Tea break
16:30–17:30 Session 6 – Tools (Chair: Fu Song)
16:30–17:00 Stefano Schivo, Bugra Mehmet Yildiz, Enno Ruijters, Christopher Gerking, Rajesh Kumar, Stefan Dziwok, Arend Rensink and Marielle Stoelinga: How to Efficiently Build a Front-End Tool for UPPAAL: A Model-Driven Approach
17:00–17:30 Idress Husien, Sven Schewe and Nicolas Berthier: PranCS: A Protocol and Discrete Controller Synthesis Tool
18:30–20:30 Banquet
Day 3：25 October 2017
08:00–09:00 Registration
09:00–10:00 Keynote 4 (Chair: Xinyu Feng)
Jean-Pierre Talpin, INRIA
Compositional methods for cyber-physical system design
10:00–10:30 Tea break
10:30–12:00 Session 7 – Modeling and verification II (Chair: Zhishan Guo)
10:30–11:00 Andrzej Mizera, Jun Pang, Hongyang Qu and Qixia Yuan: A Decomposition Method for Attractor Detection in Large Synchronous Boolean Networks
11:00–11:30 Daichi Morita, Fuyuki Ishikawa and Shinichi Honiden: Construction of Abstract State Graphs for Understanding Event-B Models
11:30–12:00 Maithily Diwan and Meenakshi D’Souza : A framework for modeling and verifying IoT communication protocols
12:00–12:15 Closing
12:15–13:45 Lunch