The 21st International Conference on Formal Engineering Methods

ICFEM 2019

November 5th-9th, 2019, Shenzhen, China

Conference Program

Wednesday November 6th
08:00–08:45 Registration
08:45–09:00 Opening (Zhong Ming / Shengchao Qin / Yamine Ait-Ameur)
09:00–10:00 Keynote talk I (Zhong Ming / Shengchao Qin)
Prof. Yang Liu: Secure Deep Learning Engineering: a Road towards Quality Assurance of Intelligent Systems
10:00–10:30 Security (Zhong Ming / Shengchao Qin)
10:00–10:30 Jialiang Chang, Bo Gao, Hao Xiao, Jun Sun, Yan Cai and Zijiang Yang: sCompile: Critical Path Identification and Analysis for Smart Contracts
10:30–11:00 Coffee break
11:00–12:30 Security, Smart Contract & User Interface (Yang Liu)
11:00–11:30 Yuan Fei, Huibiao Zhu, Haiying Sun and Jiaqi Yin: A Security Calculus for Wireless Networks of Named Data Networking
11:30–12:00 Ximeng Li, Zhiping Shi, Qianying Zhang, Guohui Wang, Yong Guan and Ning Han: Towards Verifying Ethereum Smart Contracts at Intermediate Language Level
12:00–12:30 Bohua Zhan, Zhenyan Ji, Wenfan Zhou, Chaozhu Xiang, Jie Hou and Wenhui Sun: Design of point-and-click user interfaces for proof assistants
12:30–14:00 Lunch break
14:00–15:30 Model Checking & SMT (Meng Sun)
14:00–14:30 Yueling Zhang, Geguang Pu and Min Zhang: SMTBCF: Efficient Backbone Computing for SMT Formulas
14:30–15:00 Sylvain Conchon and Mattias Roux: Reasoning about Universal Cubes in MCMT
15:00–15:30 Marko Kleine Büning and Carsten Sinz: Automatic Modularization of Large Programs for Bounded Model Checking
15:30–16:00 Coffee break
16:00–17:30 Formal modelling & Refinement & Theorem Proving (Zhe Hou)
16:00–16:30 Hui Feng, Marcello Bonsangue and Farhad Arbab: A Reo Model of Software Defined Networks
16:30–17:00 Boubacar Demba Sall, Frederic Peschanski and Emmmanuel Chailloux: A Mechanized Theory of Program Refinement
17:00–17:30 Yongjian Li and Bow-Yaw Wang: Parameterized Hardware Verification Through A Term-level Generalized Symbolic Trajectory Evaluation
Thursday November 7th
09:00–10:00 Keynote talk II (Jin Song Dong)
Prof. Luke Ong: Probabilistic Programming for Bayesian Machine Learning
10:00–10:30 Machine Learning (Jin Song Dong)
10:00–10:30 Yi Li, Xuechao Sun, Yong Li, Andrea Turrini and Lijun Zhang: Synthesizing Nested Ranking Functions for Loop Programs via SVM
10:30–11:00 Coffee break
11:00–12:30 Complex Systems, Temporal Logic and Simulations (Klaus-Dieter Schewe)
11:00–11:30 Nikola Benes, Lubos Brim, Samuel Pastva, Jakub Polacek and David Šafránek: Formal Analysis of Qualitative Long-Term Behaviour in Parametrised Boolean Networks
11:30–12:00 Leandro Gomes, Alexandre Madeira, Luis Barbosa and Manisha Jain: On the generation of equational dynamic logics for weighted imperative programs
12:00–12:30 Patrick Gardy and Yuxin Deng: Simulations for Multi-Agent Systems with imperfect information
12:30–14:00 Lunch break
14:00–15:00 Keynote talk III (Shaoying Liu)
Prof. Zhendong Su: Specification-less Semantic Bug Detection
15:00–15:30 Program Analysis (Shaoying Liu)
15:00–15:30 Xilong Zhuo and Chenyi Zhang: A Relational Static Semantics for Call Graph Construction
15:30–16:00 Coffee break
16:00–17:30 Program analysis & program synthesis (Huaikou Miao)
16:00–16:30 Ai Liu and Meng Sun: A Coalgebraic Semantics Framework for Quantum Systems
16:30–17:00 Salwa Souaf and Frederic Loulergue: A First Step in the Translation of Alloy to Coq
17:00–17:30 Lin Cheng: SqlSol: An accurate SQL Query Synthesizer
18:00–21:00 Banquet
Friday November 8th
09:00–10:00 Keynote talk IV (Yamine Ait-Ameur)
Prof. Naijun Zhan: Taming Delays in Cyber-Physical Systems
10:00–10:30 Hybrid systems (Yamine Ait-Ameur)
10:00–10:30 Bai Xue, Martin Fraenzle, Hengjun Zhao, Naijun Zhan and Arvind Easwaran: Probably Approximate Safety Verification of Hybrid Dynamical Systems
10:30–11:00 Coffee break
11:00–12:30 Formal modelling & Refinement & Theorem Proving (Sofiane Taher)
11:00–11:30 Klaus-Dieter Schewe: Consistency Enforcement for Static First-Order Invariants in Sequential Abstract State Machines
11:30–12:00 Shuangqing Xiang, Marcello Bonsangue and Huibiao Zhu: PDNet: A Programming Language for Software-Defined Networks with VLAN
12:00–12:30 Junnan Xu, Wanwei Liu, David N. Jansen and Lijun Zhang: An Axiomatisation of the Probabilistic mu-Calculus
12:30–14:00 Lunch break
14:00–15:30 Model Checking & SMT (Sylvain Conchon)
14:00–14:30 Marko Kleine Büning, Carsten Sinz and Tomas Balyo: Using DimSpec for Bounded and Unbounded Software Model Checking
14:30–15:00 Etienne Renault and Denis Poitrenaud: Combining Parallel Emptiness Checks with Partial Order Reductions
15:00–15:30 Isamu Hasegawa and Tomoyuki Yokogawa: Automatic verification for node-based visual script notation using model checking
15:30–16:00 Coffee break
16:00–17:30 Formal Verification, and Requirement Modelling (Dominique Mery)
16:00–16:30 Yassmeen Elderhalli, Osman Hasan and Sofiene Tahar: A Formally Verified Algebraic Approach for Dynamic Reliability Block Diagrams
16:30–17:00 Steve Jeffrey Tueno Fotso, Regine Laleau, Marc Frappier, Amel Mammar, Francois Thibodeau and Mama Nsangou Mouchili: Assessment of a Formal Requirements Modeling Approach on a Transportation System
17:00–17:30 Allison Sullivan, Darko Marinov and Sarfraz Khurshid: Solution Enumeration Abstraction -- A Modeling Idiom to Enhance a Lightweight Formal Method
17:30–18:00 Closing