SETTA 2023

Symposium on Dependable Software Engineering

Theories, Tools and Applications

Nanjing, China, Nov. 27-29, 2023


Keynote 1: Inferring Assertion-based Program Specifications

Prof. Nazareno Aguirre
Associate Professor
Computer Science Department
University of Rio Cuarto (UNRC), Argentina

Abstract: Analyzing software reliability requires a formal specification of the intended behavior of the software under analysis. Unfortunately, software many times lacks such specifications, and thus inferring them from existing software elements such as source code, code comments, or program executions, is important, as it can facilitate more effective software analysis. In this talk I will describe some current attempts to infer specifications at the level of source code, in the form of program assertions. I will present techniques that are able to produce program assertions based on three main tasks: (i) executing the program under analysis to obtain samples of the current program behavior, (ii) applying program/state mutation to get samples that deviate from the program behavior, and (iii) employing some generation approach to produce assertions capturing the “valid” program executions, while rejecting the “deviating” ones. The techniques differ on how these three components are realized and composed, and in particular, in the approach used for assertion generation; evolutionary search and fuzzing are two specific mechanisms that have been recently explored for this latter task. Finally, I will discuss some approaches related to specification inference, and current lines of research in this area.

Nazareno Aguirre is an Associate Professor at the University of Rio Cuarto, Argentina, and a Research Scientist at Argentina's National Council for Scientific and Technical Research (CONICET). His current research interests relate to the problem of guaranteeing software correctness and helping produce quality software, mostly via techniques for program specification, automated testing, and program verification, with formal underpinnings. Nazareno Aguirre's research has been published in top-tier software engineering conferences and journals. He regularly serves on program committees of software engineering conferences and is currently an Associate Editor of IEEE Transactions on Software Engineering.

Keynote 2: Probabilistic Model Checking for Sports Strategy Analytics

Prof. Jin Song Dong
Professor and Deputy Head
Computer Science Department
National University of Singapore, Singapore

Abstract: Sports analytics encompasses the utilization of data science, artificial intelligence (AI), psychology, and Internet of Things (IoT) devices to enhance sports performance, strategy, and decision-making. This process involves the collection, processing, and interpretation of cloud-based data from a variety of sources, such as video recordings, performance metrics, and scouting reports. The resulting insights aid in evaluating player and team performance, preventing injuries, and supporting coaches and team managers in making well-informed decisions to optimize resources and achieve superior outcomes. One widely recognized formal method, Probabilistic Model Checking (PMC), has traditionally been employed in reliability analysis for safety-critical systems. For instance, the reliability of an aircraft can be determined by evaluating the reliability of its individual components, including the engine, wings, and sensors. We apply PMC to a new application domain: Sports Strategy Analytics. As an example, the reliability (winning percentage) of a tennis player can be ascertained from the reliability (success rate) of their specific sub-skill sets (e.g., serve, forehand, backhand, etc). In this presentation, we will discuss our recent research work, which involves the application of PMC, machine learning, and computer vision to sports analytics. At the end of the presentation, we will present the vision of a new international sports analytics conference series (

Jin Song Dong is a professor and deputy head of the Computer Science Department at the National University of Singapore. His research interests include formal methods, safety and security systems, probabilistic reasoning, sports analytics, and trusted machine learning. He co-founded the commercialized PAT verification system with J. Sun and Y. Liu, which has garnered thousands of registered users from over 150 countries. Jin Song also co-founded the commercialized trusted machine learning system Silas ( with Z. Hou and H. Bride. He has received numerous best paper awards, including the ACM SIGSOFT ICSE Distinguished Paper Award. He served on the editorial board of ACM Transactions on Software Engineering and Methodology and ACM Formal Aspects of Computing. He has successfully supervised 28 PhD students, many of whom have become tenured faculty members at leading universities worldwide. He is also a Fellow of the Institute of Engineers Australia. In his leisure time, Jin Song developed Markov Decision Process (MDP) models for tennis strategy analysis using PAT, assisting professional players with pre-match analysis (outperforming the world's best). He is a Junior Grand Slam coach and coached tennis to his three children, all of whom have reached the #1 national junior ranking in Singapore/Australia. Two of his children have earned NCAA Division 1 full scholarship, while his second son, Chen Dong, played #1 singles for Australia in the Junior Davis Cup World Final and participated in both the Australian Open and US Open Junior Grand Slams.

Keynote 3: The experiences of developing the industrial-strength tools for modeling, testing and verification: a formal methods perspective

Prof. Geguang Pu
Software Engineering Institute
East China Normal University, China

Abstract: FM-related techniques are very helpful to ensure the quality of software. For instance, the model checking technique has been successfully applied in hardware/software verification and it becomes the key element for EDA tool chains. In this talk, I will share the experiences of developing the industrial-strength tools for modeling, testing and verification from the formal methods perspective. We will show how to find the real problems about testing and verification from the industry and also show how the formal methods can guide to solve these problems by developing tools. We will illustrate our experiences and insights by three interesting tools under development. The first one is a formal modeling and verification tool for the formal verification of Interlock system of the train, that is key part of signal systems in railway. The second one is a testing tool for embedded systems, where the symbolic execution technique plays an important role. The last one is a new model checking solver for hardware verification, and its performance is tuned effectively by the new observations on the search process in the state space. These tools are successfully applied in our industry partners and their effectiveness is also proved by large scale examples. Last but not least, we will also share the lessons we have learned during the tool development.

Geguang Pu is a full professor of software engineering at East China Normal University. His research interests span the areas of software modeling, automated testing, and model checking. A common thread in Geguang's research is improving software reliability and trustworthiness by developing FM-based tools. Geguang joined East China Normal Universityin 2005 as an assistant professor and prior to that, he studied for Ph. D in Peking University. In July 2018, he was appointed as CEO of Shanghai Trusted Industrial Control Platform Co., Ltd for the technique transfer, where he is leading an effective engineering teams to develop the tool chains for software modeling, testing and verification, and these tools are used by more than 100 institutes/companies for structing more reliable software systems.


All times are given in Beijing time (UTC+08:00)

Registration Location: Lobby, Golden Eagle Summit Hotel

Conference Room: Jinying Hall C, 5th Floor, Golden Eagle Summit Hotel

Day 1 (November 27, 2023)

13:30 – 20:00

Day 2 (November 28, 2023)

08:30 – 09:00
09:00 – 10:00
Keynote speaker 1
Nazareno Aguirre: Inferring Assertion-based Program Specifications
10:00 – 10:30
Coffee Break
10:30 – 11:50
Session I: Proving and Verification
10:30 – 10:50
Formalization of Lambda Calculus With Explicit Names as a Nominal Reasoning Framework
Xinyi Wan and Qinxiang Cao
10:50 – 11:10
Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof Simplification
Shenghao Yuan, Benjamin Lion, Frédéric Besson and Jean-Pierre Talpin
11:10 – 11:30
An Abstract Domain of Linear Templates with Disjunctive Right-hand-side Intervals
Han Xu, Liqian Chen, Guangsheng Fan, Banghu Yin and Ji Wang
11:30 – 11:50
Enhancing Branch and Bound for Robustness Verification of Neural Networks via An Effective Branching Strategy
Shaocong Han and Yi Zhang
12:00 – 13:00
13:30 – 14:30
Keynote speaker 2
Jin Song Dong: Probabilistic Model Checking for Sports Strategy Analytics
14:30 – 15:10
Session II: Testing of Deep Learning System
14:30 – 14:50
DeepTD: Diversity-guided Deep Neural Network Test Generation
Jin Zhu, Chuanqi Tao and Hongjing Guo
14:50 – 15:10
HeatC: A Variable-grained Coverage Criterion for Deep Learning Systems
Weidi Sun, Yuteng Lu, Xiaokun Luan and Meng Sun
15:10 – 15:40
Coffee Break
15:40 – 17:20
Session III: Testing and Vulnerability
15:40 – 16:00
SeHBPL: Behavioral semantics-based Patch Presence Test for Binaries
Jintao Huang, Gaosheng Wang, Zhiqiang Shi, Fei Lv, Weidong Zhang and Shichao Lv
16:00 – 16:20
Understanding the Reproducibility Issues of Monkey for GUI Testing
Huiyu Liu, Qichao Kong, Jue Wang, Ting Su and Haiying Sun
16:20 – 16:40
Enhance Fuzzing Oriented Binary Level Concolic Execution on Windows with Binary Level Taint Analysis and Rich Instrumentation
Yixiao Yang, Chen Gao, Zhiqi Li and Rui Wang
16:40 – 17:00
Software Vulnerability Detection Using An Enhanced Generalization Strategy
Hao Sun, Zhe Bu, Yang Xiao, Chengsheng Zhou, Zhiyu Hao and Hongsong Zhu
17:00 – 17:20
Vulnerability Report Analysis and Vulnerability Reproduction for Web Applications
Weiwei Wang, Li Zidong, You Feng and Ruilian Zhao
18:00 – 20:00

Day 3 (November 29, 2023)

09:00 – 10:00
Keynote speaker 3
Geguang Pu: The experiences of developing the industrial-strength tools for modeling, testing and verification: a formal methods perspective
10:10 – 10:30
Coffee Break
10:30 – 11:50
Session IV: Learning-Enhanced Analysis
10:30 – 10:50
Reachability Based Uniform Controllability to Target Set With Evolution Function
Jia Geng, Ruiqi Hu, Kairong Liu, Zhihui Li and Zhikun She
10:50 – 11:10
Run-time Assured Reinforcement Learning for Safe Spacecraft Rendezvous with Obstacle Avoidance
Yingmin Xiao, Zhibin Yang, Yong Zhou and Zhiqiu Huang
11:10 – 11:30
Graph-based Log Anomaly Detection via Adversarial Training
Zhangyue He, Yanni Tang, Kaiqi Zhao, Jiamou Liu and Wu Chen
11:30 – 11:50
Cheat-FlipIt: an Approach to Modeling and Perception of a Deceptive Opponent
Qian Yao, Xinli Xiong and Yongjie Wang
12:00 – 13:00
13:30 – 15:10
Session V: Behaviour, Concurrency, Coordination
13:30 – 13:50
Optimized Solutions for Highly Contended Transactional Workloads
Chunxi Zhang, Shuyan Zhang, Ting Chen, Rong Zhang, and Kai Liu
13:50 – 14:10
Leveraging TLA+ Specifications to Improve the Reliability of the ZooKeeper Coordination Service
Lingzhi Ouyang, Yu Huang, Binyu Huang and Xiaoxing Ma
14:10 – 14:30
Multi-Dimensional Abstraction and Decomposition for Separation of Concerns
Zhiming Liu, Jiadong Teng and Bo Liu
14:30 – 14:50
Session Types With Multiple Senders Single Receiver
Zekun Ji, Shuling Wang and Xiong Xu
14:50 – 15:10
Formal Verification based Synthesis for Behavior Trees
Weijiang Hong, Zhenbang Chen, Minglong Li, Yuhan Li, Peishan Huang and Ji Wang
15:10 – 15:40
Coffee Break
15:40 – 17:00
Session VI: Constraint Solving
15:40 – 16:00
Solving SMT over non-linear real arithmetic via numerical sampling and symbolic verification
Xinpeng Ni, Yulun Wu and Bican Xia
16:00 – 16:20
Modeling Regex Operators for Solving Regex Crossword Puzzles
Weihao Su, Haiming Chen, Rongchen Li and Zixuan Chen
16:20 – 16:40
Deducing Matching Strings for Real-World Regular Expressions
Yixuan Yan, Weihao Su, Lixiao Zheng, Mengxi Wang, Haiming Chen, Chengyao Peng, Rongchen Li and Zixuan Chen
16:40 – 17:00
String Constraints with Regex-Counting and String-Length Solved More Efficiently
Denghang Hu and Zhilin Wu
17:00 – 20:00
Closing & Banquet