| 2026 | AAAI | T4NMTD: Transition-Centric Reinforcement Learning for Non-Markovian Task Decomposition. | Ruixuan Miao, Xu Lu, Cong Tian, Bin Yu, Zhenhua Duan |
| 2026 | ACL | Bridging Kernel Drivers and Virtual Device Models with LLM-Powered Automation. | Mingyu Wang, Bin Yu, Wenjian Lu, Zhi Wang, Kefeng Gao, Cheng Wen, Xu Lu, Cong Tian |
| 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 | CAV | ATKVerifier: Adaptive Top-K Constraints for Tighter Verification of Semantic Segmentation Networks. | Yuehao Liu, Cong Tian, Yansong Dong, Liang Zhao, Chao Huang, Wensheng Wang |
| 2026 | CAV | Upper Bound for the Determinization of Emerson-Lei Automata: A One-Fin Approach. | Runzhe Ma, Cong Tian, Wensheng Wang, Zhenhua Duan |
| 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 | ICSE | Atomicity Violation Detection for Interrupt-Driven Programs via Incrementally Exploring Concurrent Paths. | Yuanzhe Liu, Bin Yu, Ruixue Li, Cheng Wen, Xu Lu, Chu Chen, Cong Tian |
| 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 | 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 | 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 | DASFAA | CoopKG: An Academic Knowledge Graph for Question Answering Systems. | Muyuan Niu, Cong Tian |
| 2025 | IJCAI | Neuron Similarity-Based Neural Network Verification via Abstraction and Refinement. | Yuehao Liu, Yansong Dong, Liang Zhao, Wensheng Wang, Cong Tian |
| 2025 | WWW | EdgeThemis: Ensuring Model Integrity for Edge Intelligence. | Jiyu Yang, Qiang He, Zheyu Zhou, Xiaohai Dai, Feifei Chen, Cong Tian, Yun Yang |
| 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 | DAC | DACPara: A Divide-and-Conquer Parallel Approach for High-Quality Logic Rewriting in Large-Scale Circuits. | Nanjiang Qu, Cong Tian, Zhenhua Duan |
| 2024 | ECCV | Preventing Catastrophic Overfitting in Fast Adversarial Training: A Bi-level Optimization Perspective. | Zhaoxin Wang, Handing Wang, Cong Tian, Yaochu Jin |
| 2024 | ICSOC | DynaEDI: Decentralized Integrity Verification for Dynamic Edge Data. | Qiang He, Jiyu Yang, Feifei Chen, Cong Tian, Yanhui Li, Yun Yang |
| 2024 | SETTA | A Contract-Based Framework for Formal Verification of Embedded Software. | Xu Lu, Cong Tian, Bin Gu, Bin Yu, Chen Chen, Zhenhua Duan |
| 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 | ACNS | Tiny WFP: Lightweight and Effective Website Fingerprinting via Wavelet Multi-Resolution Analysis. | Cong Tian, Dengpan Ye, Chuanxi Chen |
| 2023 | COCOA | A Dynamic Parameter Adaptive Path Planning Algorithm. | Guangyu Yao, Nan Zhang, Zhenhua Duan, Cong Tian |
| 2023 | COCOON | An Approach to Agent Path Planning Under Temporal Logic Constraints. | Chaofeng Yu, Nan Zhang, Zhenhua Duan, Cong Tian |
| 2023 | ISSTA | SBDT: Search-Based Differential Testing of Certificate Parsers in SSL/TLS Implementations. | Chu Chen, Pinghong Ren, Zhenhua Duan, Cong Tian, Xu Lu, Bin Yu |
| 2023 | TACAS | PIChecker: A POR and Interpolation based Verifier for Concurrent Programs (Competition Contribution). | Jie Su, Zuchao Yang, Hengrui Xing, Jiyu Yang, Cong Tian, Zhenhua Duan |
| 2023 | TASE | Verifying Chips Design at RTL Level. | Wu Wang, Nan Zhang, Cong Tian, Zhenhua Duan, Zhijie Xu, Chaofeng Yu |
| 2022 | QRS | An Empirical Study on Software Defect Prediction using Function Point Analysis. | Xinghan Zhao, Cong Tian |
| 2021 | QRS | Improving Quality of Counterexamples in Model Checking via Automated Planning. | Xu Lu, Cong Tian, Bin Yu, Zhenhua Duan |
| 2020 | COCOA | Transforming Multi-matching Nested Traceable Automata to Multi-matching Nested Expressions. | Jin Liu, Zhenhua Duan, Cong Tian |
| 2020 | LICS | Making Streett Determinization Tight. | Cong Tian, Wensheng Wang, Zhenhua Duan |
| 2020 | QRS | RTPDroid: Detecting Implicitly Malicious Behaviors Under Runtime Permission Model. | Jie Zhang, Cong Tian, Zhenhua Duan, Liang Zhao |
| 2019 | ICSE | FastDroid: efficient taint analysis for Android applications. | Jie Zhang, Cong Tian, Zhenhua Duan |
| 2018 | AAIM | A Novel Approach to Verifying Context Free Properties of Programs. | Nan Zhang, Zhenhua Duan, Cong Tian, Hongwei Du |
| 2018 | COCOA | Reducing Extension Edges of Concurrent Programs for Reachability Analysis. | Cong Tian, Jiaying Wang, Zhenhua Duan, Liang Zhao |
| 2018 | ICSE | RFC-directed differential testing of certificate validation in SSL/TLS implementations. | Chu Chen, Cong Tian, Zhenhua Duan, Liang Zhao |
| 2018 | ICSE | Accelerating counterexample detection in software model checking. | Cong Tian, Zhao Duan, Zhenhua Duan |
| 2018 | ICSE | Android inter-component communication analysis with intent revision. | Cong Tian, Congli Xia, Zhenhua Duan |
| 2018 | TACAS | InterpChecker: Reducing State Space via Interpolations - (Competition Contribution). | Zhao Duan, Cong Tian, Zhenhua Duan, C.-H. Luke Ong |
| 2017 | COCOA | Modeling and Verifying Multi-core Programs. | Nan Zhang, Zhenhua Duan, Cong Tian, Hongwei Du, Kai Yang |
| 2017 | COCOA | Cloning Automata: Simulation and Analysis of Computer Bacteria. | Chu Chen, Zhenhua Duan, Cong Tian, Hongwei Du |
| 2017 | ICFEM | Verifying Temporal Properties of C Programs via Lazy Abstraction. | Zhao Duan, Cong Tian, Zhenhua Duan |
| 2017 | IJCAI | Temporalising Separation Logic for Planning with Search Control Knowledge. | Xu Lu, Cong Tian, Zhenhua Duan |
| 2017 | ICSE | Full regular temporal property verification as dynamic program execution. | Meng Wang, Cong Tian, Zhenhua Duan |
| 2016 | COCOA | Using Unified Model Checking to Verify Heaps. | Xu Lu, Zhenhua Duan, Cong Tian |
| 2016 | COCOON | Satisfiability of Linear Time Mu-Calculus on Finite Traces. | Yao Liu, Zhenhua Duan, Cong Tian, Bin Cui |
| 2016 | IJCAI | A Decision Procedure for a Fragment of Linear Time Mu-Calculus. | Yao Liu, Zhenhua Duan, Cong Tian |
| 2016 | MSR | How android app developers manage power consumption?: an empirical study by mining power management commits. | Lingfeng Bao, David Lo, Xin Xia, Xinyu Wang, Cong Tian |
| 2015 | COCOA | Symbolic Model Checking for Alternating Projection Temporal Logic. | Haiyang Wang, Zhenhua Duan, Cong Tian |
| 2015 | COCOON | Model Checking MSVL Programs Based on Dynamic Symbolic Execution. | Zhenhua Duan, Kangkang Bu, Cong Tian, Nan Zhang |
| 2015 | CSCWD | Verification of a real time scheduling protocol of safety-critical systems. | Meng Wang, Zhenhua Duan, Cong Tian, Nan Zhang |
| 2015 | ICFEM | Model Checking \mu μ C/OS-III Multi-task System with TMSVL. | Jin Cui, Zhenhua Duan, Cong Tian, Nan Zhang, Conghao Zhou |
| 2014 | COCOA | Improved Even Order Magic Square Construction Algorithms and Their Applications. | Zhenhua Duan, Jin Liu, Jie Li, Cong Tian |
| 2014 | COCOON | Normal Form Expressions of Propositional Projection Temporal Logic. | Zhenhua Duan, Cong Tian, Nan Zhang |
| 2014 | COCOON | An Axiomatization for Cylinder Computation Model. | Nan Zhang, Zhenhua Duan, Cong Tian |
| 2014 | CSCWD | Simulation and verification of the virtual memory management system with MSVL. | Meng Wang, Zhenhua Duan, Cong Tian |
| 2014 | ICECCS | Model Checking Rate-Monotonic Scheduler with TMSVL. | Jin Cui, Zhenhua Duan, Cong Tian |
| 2014 | ICFEM | Extending MSVL with Function Calls. | Nan Zhang, Zhenhua Duan, Cong Tian |
| 2014 | TASE | An Improved Recursive Algorithm for Parity Games. | Yao Liu, Zhenhua Duan, Cong Tian |
| 2013 | COCOA | An Extended Strange Planet Protocol. | Jin Liu, Zhenhua Duan, Cong Tian |
| 2013 | COCOON | Bounded Model Checking for Propositional Projection Temporal Logic. | Zhenhua Duan, Cong Tian, Mengfei Yang, Jia He |
| 2013 | COCOON | Deternimization of Bchi Automata as Partitioned Automata. | Cong Tian, Zhenhua Duan, Mengfei Yang |
| 2013 | CSCWD | Simulation of CTCS-3 protocol with temporal logic programming. | Peng Zhang, Zhenhua Duan, Cong Tian |
| 2013 | ICFEM | Translation from Workflow Nets to MSVL. | Ya Shi, Zhenhua Duan, Cong Tian |
| 2013 | ICSE | Detecting spurious counterexamples efficiently in abstract model checking. | Cong Tian, Zhenhua Duan |
| 2012 | TASE | Symbolic Model Checking for Propositional Projection Temporal Logic. | Tao Pang, Zhenhua Duan, Cong Tian |
| 2011 | COCOON | Making Abstraction-Refinement Efficient in Model Checking. | Cong Tian, Zhenhua Duan |
| 2011 | ICST | Utilizing Model Checking for Automatic Test Case Generation from Conjunctions of Predicates. | Cong Tian, Shaoying Liu, Shin Nakajima |
| 2011 | TASE | Focus Game for Projection Temporal Logic. | Cong Tian, Zhenhua Duan |
| 2011 | TIME | Synthesising Classic and Interval Temporal Logic. | Sven Schewe, Cong Tian |
| 2010 | COCOA | A Transformation from PPTL to S1S. | Cong Tian, Zhenhua Duan |
| 2010 | ICFEM | An Improved Decision Procedure for Propositional Projection Temporal Logic. | Zhenhua Duan, Cong Tian |
| 2010 | ICFEM | Alternating Interval Based Temporal Logics. | Cong Tian, Zhenhua Duan |
| 2008 | ICFEM | A Unified Model Checking Approach with Projection Temporal Logic. | Zhenhua Duan, Cong Tian |
| 2008 | TAMC | Propositional Projection Temporal Logic, Bchi Automata and omega-Regular Expressions. | Cong Tian, Zhenhua Duan |
| 2007 | ICFEM | Model Checking Propositional Projection Temporal Logic Based on SPIN. | Cong Tian, Zhenhua Duan |
| 2007 | TAMC | Decidability of Propositional Projection Temporal Logic with Infinite Models. | Zhenhua Duan, Cong Tian |