| Jiandong Li and Shaoying Liu | Automated Trace Link Recovery Between Natural Language Requirements and Formal Specifications via LLMs |
| Kaicheng Shao, Yuteng Lu and Meng Sun | The Robustness Profile: A Metamorphic Testing Framework for Multi-Dimensional Evaluation of DRL Agents |
| Minghuang Lin, Weihao Lan, Lixiao Zheng and Haibo Li | Generating Non-matching Strings for Testing Regular Expressions via Complement Automaton Coverage |
| Yao Dongwen, Wu Jinhua and Wang Yuting | Clight2Rust: A Lightweight Framework for Translating a Subset of C to Safe Rust |
| Yuchen Zhang, Cheng Wen, Zhiwu Xu, Dugang Liu, Jialun Cao, Yuwei Liu, Shengchao Qin and Cong Tian | Enhancing LLM-based Proof Synthesis for Rust Programs via Semantic Chunking and Hierarchical Context Expansion |
| Jun Zhang, Xinyin Liao, Cheng Wen, Jie Su, Zhuohua Li, Yuandao Cai, Xiaoxue Ma and Shengchao Qin | Towards Accurate Thread Sharing Analysis via Synchronization-Aware Dynamic Tracing |
| Yiyuan Cao, Jiayi Zhuang, Jinkai Fan, Di Wang and Zhenjiang Hu | A HOL Theorem Proving Interface for C |
| Tayssir Touili and Olzhas Zhangeldinov | CARET Model Checking of Self Modifying Code |
| 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 | QCP: A Practical Separation Logic-based C Program Verification Tool |
| Mikael Bisgaard Dahlsen-Jensen and Jaco van de Pol | Random Generation of Small Quantitative Automata for Algorithm Debugging |
| Jianing Chen, Wanwei Liu and Ji Wang | Learning-Based Quantitative Evaluation of GR(1) Temporal Properties upon Partial Data Traces |
| Boli Huang, Tianlin Li, Ming Hu, Ziming Zhao and Mingsong Chen | Learn by Analogy: Distribution-aware Fuzz Testing for DNNs via Cross-Modal Generation |
| Xinyu Liang and Qin Li | A Formal Quantitative Approach for Evaluating Safety-Critical Driving Scenarios via Statistical Model Checking |
| Taeseung Sohn and Tsubasa Takagi | Reachable Completeness Theorem of Order-sorted Equational Logic with Infinite Proofs |
| Ling Qin, Jincao Feng and Weikai Miao | LLM-Guided Requirement Scenario-Based Testing for Simulink Models |
| Zihan Tang, Sini Chen, Lili Xiao and Huibiao Zhu | PAT2PRISM: Bridging Qualitative Correctness and Quantitative Resilience for IoT Protocols |
| Ziyun Xu, Hao Wang and Meng Sun | From Monolithic to Compositional: A Compositional Operational Semantics for Crystality |
| Tingyu Wang, Mengfei Yang, Jingjing Jiang and Hongbiao Liu | Health-State-Aware Adaptive Bad Block Management for NAND Flash-Based Storage Systems |
| Rodrigo Alves, Juliana Cunha and Alexandre Madeira | First Steps in a Paraconsistent Transition Systems Toolkit |
| Puneet Bhateja | Scenario Matching Problem in Distributed Systems |
| Shushu Wu, Xiwei Wu, Chengxi Yang and Qinxiang Cao | Intuitive Verification of Sequential Programs Using Hybrid Reasoning |
| Yi Yang, Shufang Zhu, Giuseppe De Giacomo, Qin Zhao, Xinchao Li and Dongdong An | Incremental Reinforcement Learning with Temporally Dependent Goals |
| Xiangyu Luo, Li Li, Lijun Wu, Kaile Su, Zuxi Chen and Lixiao Zheng | Symbolic Model Checking for Linear Temporal Dynamic Logic via Compositional Testers |
| Shaojie Wang, Yuting Wang, Qianying Zhang, Weituo Dai, Tian'Ao Xie, Shijun Zhao and Yongwang Zhao | Formal Verification of a Rust-Based Buddy Physical Memory Allocator (short paper) |
| Jiandong Li and Shaoying Liu | Improve Formal Specification-Based Code Review with LLMs (short paper) |
| Yuantao Hu, Shizhong Zhao, Yun Wang and Mingyuan Xia | RealSanitizer: Detecting Floating-Point Errors via a Dynamic Precision Oracle (short paper) |
| Lei Zhang and Zhiyuan Chen | Semantics-Based Verification of an Implemented Shor Oracle for ECDLP in Qrisp (short paper) |
| Andrea Manini, Matteo Rossi and Pierluigi San Pietro | Timed Games under Environmental Interference with Real-Time Objectives (short paper) |
