| 2026 | ACL | Formally Specifying the Intended Behavior of the Program: LLM-Driven Neuro-Symbolic Program Specification Synthesis. | Cheng Wen, Junjie Hu, YiKun Hu, Jie Su, Bin Yu, Dugang Liu, Zhiwu Xu, Weidi Sun, Shengchao Qin, Cong Tian |
| 2026 | FM | Automated LTL Specification Generation from Industrial Aerospace Requirements. | Zhi Ma, Xiao Liang, Cheng Wen, Rui Chen, Bin Gu, Shengchao Qin, Cong Tian, Mengfei Yang |
| 2026 | SANER | Preserving Concurrency-Revealing Seeds in Fuzzing of Concurrent Programs via Tuple-Based Coverage Evaluation. | Junjie Huang, Cheng Wen, Jie Su, Zhiwu Xu, Bin Yu, Shengchao Qin, Cong Tian |
| 2026 | SANER | How Well Does Knowledge Injection Enhance LLM-Aided Formal Protocol Modeling? | Yajia Lin, Jie Su, Cheng Wen, Rong Wang, Cong Tian, Zhenhua Dun, Shengchao Qin |
| 2026 | SANER | Synergizing LLM-Driven Semantic Reasoning with Assertion-Guided Analysis for Enhanced Vulnerability Detection. | Ying Wang, Jie Su, Cheng Wen, Rong Wang, Cong Tian, Zhenhua Dun, Shengchao Qin |
| 2026 | TASE | 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 | TASE | 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 |
| 2025 | AAAI | ICM-Assistant: Instruction-tuning Multimodal Large Language Models for Rule-based Explainable Image Content Moderation. | Mengyang Wu, Yuzhi Zhao, Jialun Cao, Mingjie Xu, Zhongming Jiang, Xuehui Wang, Qinbin Li, Guangneng Hu, Shengchao Qin, Chi-Wing Fu |
| 2025 | ACL | From Informal to Formal - Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs. | Jialun Cao, Yaojie Lu, Meiziniu Li, Haoyang Ma, Haokun Li, Mengda He, Cheng Wen, Le Sun, Hongyu Zhang, Shengchao Qin, Shing-Chi Cheung, Cong Tian |
| 2025 | EMNLP | KG-RAG: Enhancing GUI Agent Decision-Making via Knowledge Graph-Driven Retrieval-Augmented Generation. | Ziyi Guan, Jason Chun Lok Li, Zhijian Hou, Pingping Zhang, Donglai Xu, Yuzhi Zhao, Mengyang Wu, Jinpeng Chen, Thanh-Toan Nguyen, Pengfei Xian, Wenao Ma, Shengchao Qin, Graziano Chesi, Ngai Wong |
| 2025 | INFOCOM | Formally Verifying the State Machine of TLS 1.3 Handshake in OpenSSL. | Jingjing Guan, Hui Li, Xiangdong Li, Xiaolei Wang, Binghan Wang, Qiuye Wang, Shengchao Qin, Mengda He, Md. Armanuzzaman, Ziming Zhao |
| 2025 | ICSE | LLM-Aided Automatic Modeling for Security Protocol Verification. | Ziyu Mao, Jingyi Wang, Jun Sun, Shengchao Qin, Jiawen Xiong |
| 2024 | CAV | Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification. | Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, Cong Tian |
| 2024 | ICFEM | Graph Convolutional Network Robustness Verification Algorithm Based on Dual Approximation. | Dongdong An, Hao Zhang, Qin Zhao, Jing Liu, Jianqi Shi, Yanhong Huang, Yang Yang, Xu Liu, Shengchao Qin |
| 2024 | ICFEM | MemSpate: Memory Usage Protocol Guided Fuzzing. | Zhiyuan Fu, Jiacheng Jiang, Cheng Wen, Zhiwu Xu, Shengchao Qin |
| 2024 | ICFEM | NL2CTL: Automatic Generation of Formal Requirements Specifications via Large Language Models. | Mengyan Zhao, Ran Tao, Yanhong Huang, Jianqi Shi, Shengchao Qin, Yang Yang |
| 2024 | ICSE | RPG: Rust Library Fuzzing with Pool-based Fuzz Target Generation and Generic Support. | Zhiwu Xu, Bohao Wu, Cheng Wen, Bin Zhang, Shengchao Qin, Mengda He |
| 2024 | TASE | CtxFuzz: Discovering Heap-Based Memory Vulnerabilities Through Context Heap Operation Sequence Guided Fuzzing. | Jiacheng Jiang, Cheng Wen, Shengchao Qin |
| 2024 | TASE | CFStra: Enhancing Configurable Program Analysis Through LLM-Driven Strategy Selection Based on Code Features. | Jie Su, Liansai Deng, Cheng Wen, Shengchao Qin, Cong Tian |
| 2023 | TASE | Detecting API-Misuse Based on Pattern Mining via API Usage Graph with Parameters. | Yulin Wu, Zhiwu Xu, Shengchao Qin |
| 2022 | COMPSAC | Algebraic Semantics for C++11 Memory Model. | Lili Xiao, Huibiao Zhu, Mengda He, Shengchao Qin |
| 2022 | ICSE | Controlled Concurrency Testing via Periodical Scheduling. | Cheng Wen, Mengda He, Bohao Wu, Zhiwu Xu, Shengchao Qin |
| 2021 | TASE | A Timed Automata based Automatic Framework for Verifying STL Properties of Simulink Models. | Miao Tian, Jianqi Shi, Zhe Hou, Yanhong Huang, Shengchao Qin |
| 2020 | ICRA | Navigating Discrete Difference Equation Governed WMR by Virtual Linear Leader Guided HMPC. | Chao Huang, Xin Chen, Enyi Tang, Mengda He, Lei Bu, Shengchao Qin, Yifeng Zeng |
| 2020 | ICSE | Typestate-guided fuzzer for discovering use-after-free vulnerabilities. | Haijun Wang, Xiaofei Xie, Yi Li, Cheng Wen, Yuekang Li, Yang Liu, Shengchao Qin, Hongxu Chen, Yulei Sui |
| 2020 | ICSE | MemLock: memory usage guided fuzzing. | Cheng Wen, Haijun Wang, Yuekang Li, Shengchao Qin, Yang Liu, Zhiwu Xu, Hongxu Chen, Xiaofei Xie, Geguang Pu, Ting Liu |
| 2020 | TASE | Analyzing Cryptographic API Usages for Android Applications Using HMM and N-Gram. | Zhiwu Xu, Xiongya Hu, Yida Tao, Shengchao Qin |
| 2020 | TASE | An Axiomatic Approach to BigrTiMo. | Wanling Xie, Huibiao Zhu, Shengchao Qin |
| 2019 | ATVA | Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation. | Long H. Pham, Quang Loc Le, Quoc-Sang Phan, Jun Sun, Shengchao Qin |
| 2019 | ICECCS | Bi-Abductive Inference for Shape and Ordering Properties. | Christopher Curry, Quang Loc Le, Shengchao Qin |
| 2018 | APLAS | Automated Modular Verification for Relaxed Communication Protocols. | Andreea Costea, Wei-Ngan Chin, Shengchao Qin, Florin Craciun |
| 2018 | FM | Towards 'Verifying' a Water Treatment System. | Jingyi Wang, Jun Sun, Yifan Jia, Shengchao Qin, Zhiwu Xu |
| 2018 | ICECCS | Variant Region Types. | Florin Craciun, Wei-Ngan Chin, Shengchao Qin |
| 2018 | ICFEM | UTP Semantics for BigrTiMo. | Wanling Xie, Huibiao Zhu, Shengchao Qin |
| 2018 | ICFEM | CDGDroid: Android Malware Detection Based on Deep Learning Using CFG and DFG. | Zhiwu Xu, Kerong Ren, Shengchao Qin, Florin Craciun |
| 2018 | ICSE | Testing heap-based programs with Java StarFinder. | Long H. Pham, Quang Loc Le, Quoc-Sang Phan, Jun Sun, Shengchao Qin |
| 2018 | TACAS | Frame Inference for Inductive Entailment Proofs in Separation Logic. | Quang Loc Le, Jun Sun, Shengchao Qin |
| 2018 | TASE | Towards a Program Logic for C11 Release-Sequences. | Mengda He, Shengchao Qin, Joo F. Ferreira |
| 2017 | ICFEM | Detecting Energy Bugs in Android Apps Using Static Analysis. | Hao Jiang, Hongli Yang, Shengchao Qin, Zhendong Su, Jian Zhang, Jun Yan |
| 2017 | ICFEM | Improving Probability Estimation Through Active Probabilistic Model Learning. | Jingyi Wang, Xiaohong Chen, Jun Sun, Shengchao Qin |
| 2017 | ICFEM | Learning Types for Binaries. | Zhiwu Xu, Cheng Wen, Shengchao Qin |
| 2017 | IJCAI | Switched Linear Multi-Robot Navigation Using Hierarchical Model Predictive Control. | Chao Huang, Xin Chen, Yifan Zhang, Shengchao Qin, Yifeng Zeng, Xuandong Li |
| 2017 | TASE | Time-sensitive information flow control in timed event-B. | Chunyan Mu, Shengchao Qin |
| 2016 | APSEC | Formalization and Verification of the Powerlink Protocol Using CSP. | Haiping Pang, Ju Li, Yijia Ruan, Yanhong Huang, Jianqi Shi, Shengchao Qin |
| 2016 | ICECCS | Concurrent On-the-Fly SCC Detection for Automata-Based Model Checking with Fairness Assumption. | Zhimin Wu, Yi Xu, Akin Gnay, Yang Liu, Shengchao Qin |
| 2016 | IJCAI | Hierarchical Model Predictive Control for Multi-Robot Navigation. | Chao Huang, Xin Chen, Yifan Zhang, Shengchao Qin, Yifeng Zeng, Xuandong Li |
| 2016 | PDP | Reasoning about Fences and Relaxed Atomics. | Mengda He, Viktor Vafeiadis, Shengchao Qin, Joo F. Ferreira |
| 2016 | TASE | State-Taint Analysis for Detecting Resource Bugs. | Zhiwu Xu, Dongxiao Fan, Shengchao Qin |
| 2015 | AAAI | On Information Coverage for Location Category Based Point-of-Interest Recommendation. | Xuefeng Chen, Yifeng Zeng, Gao Cong, Shengchao Qin, Yanping Xiang, Yuanshun Dai |
| 2015 | ICECCS | Probabilistic Denotational Semantics for an Interrupt Modelling Language. | Yanhong Huang, Yongxin Zhao, Shengchao Qin, Jifeng He |
| 2015 | ICECCS | GPU Accelerated On-the-Fly Reachability Checking. | Zhimin Wu, Yang Liu, Jun Sun, Jianqi Shi, Shengchao Qin |
| 2015 | IJCAI | Optimal Route Search with the Coverage of Users' Preferences. | Yifeng Zeng, Xuefeng Chen, Xin Cao, Shengchao Qin, Marc Cavazza, Yanping Xiang |
| 2015 | PLDI | Termination and non-termination specification inference. | Ton Chanh Le, Shengchao Qin, Wei-Ngan Chin |
| 2014 | CAV | Shape Analysis via Second-Order Bi-Abduction. | Quang Loc Le, Cristian Gherghina, Shengchao Qin, Wei-Ngan Chin |
| 2014 | TASE | Choreography Scenario-Based Test Data Generation. | Kai Ma, Jin Wang, Hongli Yang, Jun Yan, Jian Zhang, Shengchao Qin |
| 2013 | APSEC | Data-Race-Freedom of Concurrent Programs. | Granville Barnett, Shengchao Qin |
| 2013 | APSEC | Linking the Semantics of BPEL Using Maude. | Peng Liu, Huibiao Zhu, Shengchao Qin, Phillip J. Brooke, Xi Wu |
| 2013 | EMSOFT | Verifying Simulink diagrams via a Hybrid Hoare Logic Prover. | Liang Zou, Naijun Zhan, Shuling Wang, Martin Frnzle, Shengchao Qin |
| 2013 | ICECCS | Linking Algebraic Semantics and Operational Semantics for Web Services Using Maude. | Peng Liu, Huibiao Zhu, Shengchao Qin, Phillip J. Brooke, Xi Wu |
| 2013 | ICFEM | Automated Specification Discovery via User-Defined Predicates. | Guanhua He, Shengchao Qin, Wei-Ngan Chin, Florin Craciun |
| 2013 | ICFEM | Deadline Analysis of AUTOSAR OS Periodic Tasks in the Presence of Interrupts. | Yanhong Huang, Joo F. Ferreira, Guanhua He, Shengchao Qin, Jifeng He |
| 2013 | ICFEM | A UTP Semantics for Communicating Processes with Shared Variables. | Ling Shi, Yongxin Zhao, Yang Liu, Jun Sun, Jin Song Dong, Shengchao Qin |
| 2012 | ICFEM | A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs. | Granville Barnett, Shengchao Qin |
| 2012 | SEFM | The Rely/Guarantee Approach to Verifying Concurrent BPEL Programs. | Huibiao Zhu, Qiwen Xu, Chris Ma, Shengchao Qin, Zongyan Qiu |
| 2012 | SEW | A Timed CSP Model for the Time-Triggered Language Giotto. | Yanhong Huang, Yongxin Zhao, Shengchao Qin, Guanhua He, Joo F. Ferreira |
| 2012 | TASE | LBI Cut Elimination Proof with BI-MultiCut. | Ryuta Arisaka, Shengchao Qin |
| 2012 | TASE | Moverness for Locks and Transactions. | Granville Barnett, Shengchao Qin |
| 2012 | TASE | Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK. | Joo F. Ferreira, Guanhua He, Shengchao Qin |
| 2011 | CAV | A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification. | Wei-Ngan Chin, Cristian Gherghina, Razvan Voicu, Quang Loc Le, Florin Craciun, Shengchao Qin |
| 2011 | FM | Structured Specifications for Better Verification of Heap-Manipulating Programs. | Cristian Gherghina, Cristina David, Shengchao Qin, Wei-Ngan Chin |
| 2011 | FM | Automatically Refining Partial Specifications for Program Verification. | Shengchao Qin, Chenguang Luo, Wei-Ngan Chin, Guanhua He |
| 2011 | TASE | Towards an Axiomatic Verification System for JavaScript. | Shengchao Qin, Aziem Chawdhary, Wei Xiong, Malcolm Munro, Zongyan Qiu, Huibiao Zhu |
| 2010 | CADE | Discovering Specifications for Unknown Procedures - Work in Progress. | Florin Craciun, Chenguang Luo, Guanhua He, Shengchao Qin, Wei-Ngan Chin |
| 2010 | ICFEM | Loop Invariant Synthesis in a Combined Domain. | Shengchao Qin, Guanhua He, Chenguang Luo, Wei-Ngan Chin |
| 2010 | ICFEM | Verifying Heap-Manipulating Programs with Unknown Procedure Calls. | Shengchao Qin, Chenguang Luo, Guanhua He, Florin Craciun, Wei-Ngan Chin |
| 2010 | TASE | Stack Bound Inference for Abstract Java Bytecode. | Shengyi Wang, Zongyan Qiu, Shengchao Qin, Wei-Ngan Chin |
| 2009 | ATVA | Memory Usage Verification Using Hip/Sleek. | Guanhua He, Shengchao Qin, Chenguang Luo, Wei-Ngan Chin |
| 2009 | ESOP | An Interval-Based Inference of Variant Parametric Types. | Florin Craciun, Wei-Ngan Chin, Guanhua He, Shengchao Qin |
| 2008 | APSEC | A Heap Model for Java Bytecode to Support Separation Logic. | Chenguang Luo, Guanhua He, Shengchao Qin |
| 2008 | ICFEM | A Formal Soundness Proof of Region-Based Memory Management for Object-Oriented Paradigm. | Florin Craciun, Shengchao Qin, Wei-Ngan Chin |
| 2008 | POPL | Enhancing modular OO verification with separation logic. | Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin |
| 2008 | TASE | Verifying BPEL-Like Programs with Hoare Logic. | Chenguang Luo, Shengchao Qin, Zongyan Qiu |
| 2007 | ICECCS | Automated Verification of Shape, Size and Bag Properties. | Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin |
| 2007 | ICECCS | Linking Object-Z with Spec#. | Shengchao Qin, Guanhua He |
| 2007 | TASE | Realizing Live Sequence Charts in SystemVerilog. | Hai H. Wang, Shengchao Qin, Jun Sun, Jin Song Dong |
| 2007 | VMCAI | Automated Verification of Shape and Size Properties Via Separation Logic. | Huu Hai Nguyen, Cristina David, Shengchao Qin, Wei-Ngan Chin |
| 2006 | ICSE | HighSpec: a tool for building and checking OZTA models. | Jin Song Dong, Ping Hao, Xian Zhang, Shengchao Qin |
| 2006 | SEW | Integrating Probability with Time and Shared-Variable Concurrency. | Huibiao Zhu, Shengchao Qin, Jifeng He, Jonathan P. Bowen |
| 2005 | ICFEM | The Semantics and Tool Support of OZTA. | Jin Song Dong, Ping Hao, Shengchao Qin, Xian Zhang |
| 2005 | ICSE | Verifying safety policies with size properties and alias controls. | Wei-Ngan Chin, Siau-Cheng Khoo, Shengchao Qin, Corneliu Popeea, Huu Hai Nguyen |
| 2005 | SAS | Memory Usage Verification for OO Programs. | Wei-Ngan Chin, Huu Hai Nguyen, Shengchao Qin, Martin C. Rinard |
| 2004 | APLAS | A Relational Model for Object-Oriented Designs. | Jifeng He, Zhiming Liu, Xiaoshan Li, Shengchao Qin |
| 2004 | ICFEM | Timed Patterns: TCOZ to Timed Automata. | Jin Song Dong, Ping Hao, Shengchao Qin, Jun Sun, Wang Yi |
| 2004 | ICTAC | An Automatic Mapping from Statecharts to Verilog. | Viet-Anh Vu Tran, Shengchao Qin, Wei-Ngan Chin |
| 2004 | IFM | Generating MSCs from an Integrated Formal Specification Language. | Jin Song Dong, Shengchao Qin, Jun Sun |
| 2004 | PLDI | Region inference for an object-oriented language. | Wei-Ngan Chin, Florin Craciun, Shengchao Qin, Martin C. Rinard |
| 2003 | FM | Mapping Statecharts to Verilog for Hardware/Software Co-specification. | Shengchao Qin, Wei-Ngan Chin |
| 2003 | FM | A Semantic Foundation for TCOZ in Unifying Theories of Programming. | Shengchao Qin, Jin Song Dong, Wei-Ngan Chin |
| 2003 | ICFEM | The Equivalence of Statecharts. | Quan Long, Zongyan Qiu, Shengchao Qin |
| 2002 | ICFEM | Hardware/Software Partitioning in Verilog. | Shengchao Qin, Jifeng He, Zongyan Qiu, Naixiao Zhang |
| 2001 | APSEC | Partitioning Program into Hardware and Software. | Shengchao Qin, Jifeng He |