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