| 2025 | Neural-Symbolic System Control Adjustment Based on Runtime Verification. | Hongxu Zhu, Wanwei Liu, Ji Wang |
| 2025 | Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks. | Kangfeng Ye, Roberto Metere, Jim Woodcock, Poonam Yadav |
| 2025 | Formal Modeling and Verification of Blockchain Consensus Protocols: A Case Study on ChainMaker. | Minfan Xu, Shuo Zhou, Xian Xu, Huan Long |
| 2025 | Modeling and Analysis of Cyber-Physical Systems in the Hybrid π-Calculus Using Extended Sequence Diagrams. | Xiong Xu, Jixiang Miao, Shuling Wang, Jean-Pierre Talpin |
| 2025 | LLM-SYM: Integrating Symbolic Methods and Large Language Models for Automated Theorem Proving. | Yifan Wu, Yanhong Huang, Jianqi Shi |
| 2025 | ZK-ProVer: Proving Programming Verification in Non-interactive Zero-Knowledge Proofs. | Haoyu Wei, Jingyu Ke, Ruibang Liu, Guoqiang Li |
| 2025 | Modeling and Verifying Concurrent Reactive Systems Using Separation Logic. | Huan Sun, David Sann, Jun Sun, Wenhai Wang |
| 2025 | MetaLogic: Robustness Evaluation of Text-to-Image Models via Logically Equivalent Prompts. | Yifan Shen, Yangyang Shu, Hye-young Paik, Yulei Sui |
| 2025 | Formal Construction of Threat Detections from Attack Trees. | Dumitru-Bogdan Prelipcean, Catalin Dima, Daniele Varacca |
| 2025 | Avoiding Larger Conflict Regions in CDCL-Style Methods for Solving SMT-NRA. | Xinpeng Ni, Tianyi Ding, Bican Xia |
| 2025 | Formalizing Requirements into Dafny Specifications with LLMs. | Yi-Han Lu, Xue-Yang Zhu, Wenhui Zhang, Rongjie Yan |
| 2025 | Automata-Based Steering of Large Language Models for Diverse Structured Generation. | Xiaokun Luan, Zemin Wei, Yihao Zhang, Meng Sun |
| 2025 | A Test-Driven Approach for Refining Use Case Specifications of Software Requirements with LLMs. | Haibo Li, Lixiao Zheng, Qihang Cai |
| 2025 | Quantitative Verification for Temporal Properties of Massive Linear Systems. | Qing Liu, Yuntao Li, Sungwoo Choi, Luan Viet Nguyen, Hoang-Dung Tran |
| 2025 | Detecting Vector Container Errors in C++ Programs via Abstract Interpretation. | Siyu Liu, Liqian Chen, Guangsheng Fan, Banghu Yin, Chun Huang, Ji Wang |
| 2025 | Towards High-Level SMT Program Modeling: Bounded Integers, Simplified Structs, and Metaprogramming. | Xiangyu Li |
| 2025 | Formal Modelling of Fault Tolerant Robotic Missions. | Manon Lecart, Elena Troubitsyna |
| 2025 | A Unified Method to Efficiently Verify Opacity of Discrete-Timed Automata. | Julian Klein, Kuize Zhang, Sabine Glesner |
| 2025 | Synthesizing Loops from Linear Ranking Functions. | Rui-Juan Jing, Yaru Yuan, Yuxing Cai, Yi Li, Changbo Chen |
| 2025 | Formal Modeling of Reinforcement Learning Systems with SMT. | Tianyi Ding, Yuxin Lin, Meng Sun |
| 2025 | BCCIC3: Batch Clause Construction Enhanced Generalization in IC3. | Yi Chen, Xinyi Gong, Liangze Yin, Ji Wang, Ting Wang |
| 2024 | NL2CTL: Automatic Generation of Formal Requirements Specifications via Large Language Models. | Mengyan Zhao, Ran Tao, Yanhong Huang, Jianqi Shi, Shengchao Qin, Yang Yang |
| 2024 | Model Checking Concurrency in Smart Contracts with a Case Study of Safe Remote Purchase. | Yisong Yu, Naipeng Dong, Zhe Hou, Jin Song Dong |
| 2024 | Observability of Boolean Control Networks: New Definition and Verification Algorithm. | Guisen Wu, Zhiming Liu, Jun Pang |
| 2024 | Clock-Dependent Probabilistic Timed Automata with One Clock and No Memory. | Jeremy Sproston |