Program
Monday Schedule
| Time | Session | Talk |
|---|---|---|
| 9:00 – 10:00 | Invited talk by Konstantinos Sagonas Session Chair: Philipp Rümmer |
Optimal Algorithms for Stateless Model Checking |
| 10:00 – 10:30 | Program Verification Session Chair: Philipp Rümmer |
Testing-Based Formal Verification with Program Slicing on Functional Soundness and Completeness Ai Liu, Yang Liu, Shaoying Liu and Zhibin Yang |
| Coffee break | ||
| 11:00 – 11:30 | Program Verification Session Chair: Konstantinos Sagonas |
Dependent Assertion Logic for Modular Software Verification Lukas Grätz |
| 11:30 – 12:00 | A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms Chengxi Yang, Shushu Wu and Qinxiang Cao |
|
| 12:00 – 12:30 | Machine-Checked Compositional Specification and Proofs for Embedded Systems Karl Palmskog, Mattias Nyberg and Dilian Gurov |
|
| Lunch break | ||
| 14:00 – 14:30 | Verification and Concurrency Session Chair: Shaoying Liu |
Failure divergence refinement for Event-B Sebastian Stock, Michael Leuschel and Atif Mashkoor |
| 14:30 – 15:00 | Mining Diamonds in labeled Transition Systems Flip van Spaendonck and Kevin Jilissen |
|
| 15:00 – 15:30 | Portability of Optimizations from SC to TSO Akshay Gopalakrishnan and Clark Verbrugge |
|
| Coffee break | ||
| 16:00 – 16:30 | SAT and SMT Solving Session Chair: Lucas C. Cordeiro |
Adaptive Clause Management in SMT Solvers: A Dynamic Weighting Framework for Formal Verification Wenda Leng, Meihua Liu and Yufeng Jin |
| 16:30 – 17:00 | SNRWLS: Improve (W)PMS Solver with Weighting Strategies Related to Number of Soft Clauses Chen Shuhao, Jiang Menghua and Chen Yin |
|
| 19:00 – 20:30 | Welcome Reception | |
Tuesday Schedule
| Time | Session | Talk |
|---|---|---|
| 9:00 – 10:00 | Invited talk by Min Zhang Session Chair: Zhilin Wu |
Safeguarding deep reinforcement learning systems via formal methods: From safety-by-design to runtime assurance |
| 10:00 – 10:30 | Trustworthy AI and System Software Session Chair: Zhilin Wu |
Robust Deep Reinforcement Learning Using Formal Verification Avraham Raviv, Shaiel Vistuch, Erel Dekel, Boaz Gurevich and Hillel Kugler |
| Coffee break | ||
| 11:00 – 11:30 | Trustworthy AI and System Software Session Chair: Min Zhang |
A Formally Verified Neural Network Converter for the Interactive Theorem Prover Coq Leo Alexander Gummersbach, Kim Völlinger and Andrei Aleksandrov |
| 11:30 – 12:00 | COMPASS: An Agent for MLIR Compilation Pass Pipeline Generation Hongbin Zhang, Shihao Gao, Yang Liu, Mingjie Xing, Yanjun Wu and Chen Zhao |
|
| 12:00 – 12:30 | Stable Ranges: Shared Dichotomy in Large Version-Controlled Repositories Laurent Bulteau, Pierre-Yves David, Florian Horn and Euxane Tran-Girard |
|
| Lunch break | ||
| 14:00 – 14:30 | Program Analysis using ML Session Chair: Hillel Kugler |
CASTLE: Benchmarking Dataset for Static Code Analyzers and LLMs towards CWE Detection Richard A. Dubniczky, Krisztofer Zoltán Horvát, Tamás Bisztray, Mohamed Amine Ferrag, Lucas C. Cordeiro and Norbert Tihanyi |
| 14:30 – 15:00 | FAMiT: Mitigating False Alarms for Program Analysis Using Large Language Models (Short paper) Jiabao Zeng, Yuanlin Li, Ran Zhang, Yuanmin Xie, Kejia Li and Min Zhou |
|
| 17:15 | Tour & Dinner | |
Wednesday Schedule
| Time | Session | Talk |
|---|---|---|
| 9:00 – 9:30 | Security Session Chair: Karl Palmskog |
A Cross-domain Data Sharing Scheme Based on Federated Blockchain Honglin Mao, Jie Zhang, Yao Zhang and Xiaohong Li |
| 9:30 – 10:00 | Operational Semantics for Crystality: A Smart Contract Language for Parallel EVMs Ziyun Xu, Hao Wang and Meng Sun |
|
| 10:00 – 10:30 | Detecting speculative data flow vulnerabilities using weakest precondition reasoning Graeme Smith |
|
| Coffee break | ||
| 11:00 – 11:30 | Dynamic Analysis Session Chair: Graeme Smith |
Random Testing of Model Checkers for Timed Automata with Automated Oracle Generation Andrea Manini, Matteo Rossi and Pierluigi San Pietro |
| 11:30 – 12:00 | State Significance-Guided Fuzzing for Stateful Protocol Program Kunpeng Jian, Yanyan Zou, Chen Wang, Ning Li, Menghao Li and Wei Huo |
|
| 12:00 – 12:30 | Unleash the Hidden Power of CAR-based Model Checking through Dynamic Traversal Yibo Dong, Yu Chen, Jianwen Li and Geguang Pu |
|