Day 1 (July 4, 2026)Venue: Dishui Lake International Software Institute |
||
 |
08:30-09:00 | Registration |
|
09:00-09:20 | Opening Ceremony |
|
09:20-10:20 |
Keynote I Session Chair: TBD The OPERA Framework: Formal Design of Railways Interlocking Systems Alessandro Cimatti (Fondazione Bruno Kessler) |
|
10:20-10:40 | Coffee Break |
|
10:40-12:00 |
Session 1: Formal Verification and Model Checking Session Chair: TBD |
|
10:40-11:10 CARET Model Checking of Self Modifying Code Tayssir Touili and Olzhas Zhangeldinov |
||
|
11:10-11:40 Symbolic Model Checking for Linear Temporal Dynamic Logic via Compositional Testers Xiangyu Luo, Li Li, Lijun Wu, Kaile Su, Zuxi Chen and Lixiao Zheng |
||
|
11:40-12:00 Timed Games under Environmental Interference with Real-Time Objectives< Andrea Manini, Matteo Rossi and Pierluigi San Pietro |
||
|
12:00-13:30 | Lunch Break |
|
13:30-15:00 |
Session 2: Program Verification and Theorem Proving Session Chair: TBD |
|
13:30-14:00 A HOL Theorem Proving Interface for C Yiyuan Cao, Jiayi Zhuang, Jinkai Fan, Di Wang and Zhenjiang Hu |
||
|
14:00-14:30 QCP: A Practical Separation Logic-based C Program Verification Tool Xiwei Wu, Yueyang Feng, Xiaoyang Lu, Tianchuan Lin, Kan Liu, Zhiyi Wang, Shushu Wu, Lihan Xie, Chengxi Yang, Hongyi Zhong, Zihan Zhang, Juanru Li, Naijun Zhan and Qinxiang Cao |
||
|
14:30-15:00 Intuitive Verification of Sequential Programs Using Hybrid Reasoning Shushu Wu, Xiwei Wu, Chengxi Yang and Qinxiang Cao |
||
|
15:00-15:20 | Coffee Break |
|
15:20-16:50 |
Session 3: Programming Languages and Semantics Session Chair: TBD |
|
15:20-15:50 Clight2Rust: A Lightweight Framework for Translating a Subset of C to Safe Rust Yao Dongwen, Wu Jinhua and Wang Yuting |
||
|
15:50-16:20 Reachable Completeness Theorem of Order-sorted Equational Logic with Infinite Proofs Taeseung Sohn and Tsubasa Takagi |
||
|
16:20-16:50 From Monolithic to Compositional: A Compositional Operational Semantics for Crystality Ziyun Xu, Hao Wang and Meng Sun |
||
|
18:30-20:30 | Welcome Reception |
Day 2 (July 5, 2026)Venue: Dishui Lake International Software Institute |
||
|
09:00-10:00 |
Keynote II Session Chair: TBD Building Trustworthy AI Agents: Challenges and Attempts Jun Sun (Singapore Management University) |
|
10:00-10:20 | Coffee Break |
|
10:20-12:10 |
Session 4: AI for Software Engineering and LLM-based Methods Session Chair: TBD |
|
10:20-10:50 Automated Trace Link Recovery Between Natural Language Requirements and Formal Specifications via LLMs Jiandong Li and Shaoying Liu |
||
|
10:50-11:20 Enhancing LLM-based Proof Synthesis for Rust Programs via Semantic Chunking and Hierarchical Context Expansion Yuchen Zhang, Cheng Wen, Zhiwu Xu, Dugang Liu, Jialun Cao, Yuwei Liu, Shengchao Qin and Cong Tian |
||
|
11:20-11:50 LLM-Guided Requirement Scenario-Based Testing for Simulink Models Ling Qin, Jincao Feng and Weikai Miao |
||
|
11:50-12:10 Improve Formal Specification-Based Code Review with LLMs Jiandong Li and Shaoying Liu |
||
|
12:10-13:30 | Lunch Break |
|
13:30-15:00 |
Session 5: Testing, Fuzzing and Dynamic Analysis Session Chair: TBD |
|
13:30-14:00 The Robustness Profile: A Metamorphic Testing Framework for Multi-Dimensional Evaluation of DRL Agents Kaicheng Shao, Yuteng Lu and Meng Sun |
||
|
14:00-14:30 Generating Non-matching Strings for Testing Regular Expressions via Complement Automaton Coverage Minghuang Lin, Weihao Lan, Lixiao Zheng and Haibo Li |
||
|
14:30-15:00 Learn by Analogy: Distribution-aware Fuzz Testing for DNNs via Cross-Modal Generation Boli Huang, Tianlin Li, Ming Hu, Ziming Zhao and Mingsong Chen |
||
|
15:00-15:20 | Coffee Break |
|
15:20-16:40 |
Session 6: Runtime Analysis and Systems Session Chair: TBD |
|
15:20-15:50 Towards Accurate Thread Sharing Analysis via Synchronization-Aware Dynamic Tracing Jun Zhang, Xinyin Liao, Cheng Wen, Jie Su, Zhuohua Li, Yuandao Cai, Xiaoxue Ma and Shengchao Qin |
||
|
15:50-16:20 Health-State-Aware Adaptive Bad Block Management for NAND Flash-Based Storage Systems Tingyu Wang, Mengfei Yang, Jingjing Jiang and Hongbiao Liu |
||
|
16:20-16:40 RealSanitizer: Detecting Floating-Point Errors via a Dynamic Precision Oracle Yuantao Hu, Shizhong Zhao, Yun Wang and Mingyuan Xia |
||
|
17:00-18:00 | Gedenkschrift for Jean-Raymond Abrial |
|
18:30-20:30 | Conference Banquet |
Day 3 (July 6, 2026)Venue: Dishui Lake International Software Institute |
||
|
09:00-10:00 |
Keynote III Session Chair: TBD Neural Proofs for Sound Verification of Complex Programs and Systems Alessandro Abate (University of Oxford) |
|
10:00-10:20 | Coffee Break |
|
10:20-12:20 |
Session 7: Quantitative Verification and Probabilistic Analysis Session Chair: TBD |
|
10:20-10:50 Learning-Based Quantitative Evaluation of GR(1) Temporal Properties upon Partial Data Traces Jianing Chen, Wanwei Liu and Ji Wang |
||
|
10:50-11:20 A Formal Quantitative Approach for Evaluating Safety-Critical Driving Scenarios via Statistical Model Checking Xinyu Liang and Qin Li |
||
|
11:20-11:50 PAT2PRISM: Bridging Qualitative Correctness and Quantitative Resilience for IoT Protocols Zihan Tang, Sini Chen, Lili Xiao and Huibiao Zhu |
||
|
11:50-12:20 Incremental Reinforcement Learning with Temporally Dependent Goals Yi Yang, Shufang Zhu, Giuseppe De Giacomo, Qin Zhao, Xinchao Li and Dongdong An |
||
|
12:20-13:30 | Lunch Break |
|
13:30-14:30 |
Keynote IV Session Chair: TBD Abstraction and Refinement for Modelling and Analysis in Cyber Physical System Design Michael Butler (University of Southampton) |
|
14:30-14:50 | Coffee Break |
|
14:50-16:20 |
Session 8: Tools, Frameworks and Applications Session Chair: TBD |
|
14:50-15:20 Random Generation of Small Quantitative Automata for Algorithm Debugging Mikael Bisgaard Dahlsen-Jensen and Jaco van de Pol |
||
|
15:20-15:50 First Steps in a Paraconsistent Transition Systems Toolkit Rodrigo Alves, Juliana Cunha and Alexandre Madeira |
||
|
15:50-16:20 Scenario Matching Problem in Distributed Systems Puneet Bhateja |
||
|
16:20-16:40 | Coffee Break |
|
16:40-17:20 |
Session 9: Security and Formal Assurance Session Chair: TBD |
|
16:40-17:00 Formal Verification of a Rust-Based Buddy Physical Memory Allocator Shaojie Wang, Yuting Wang, Qianying Zhang, Weituo Dai, Tian'Ao Xie, Shijun Zhao and Yongwang Zhao |
||
|
17:00-17:20 Semantics-Based Verification of an Implemented Shor Oracle for ECDLP in Qrisp Lei Zhang and Zhiyuan Chen |
||
|
17:20-17:50 | Closing Remarks |