| 2026 | AAAI | T4NMTD: Transition-Centric Reinforcement Learning for Non-Markovian Task Decomposition. | Ruixuan Miao, Xu Lu, Cong Tian, Bin Yu, Zhenhua Duan |
| 2026 | CAV | Upper Bound for the Determinization of Emerson-Lei Automata: A One-Fin Approach. | Runzhe Ma, Cong Tian, Wensheng Wang, Zhenhua Duan |
| 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 | 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 | An Approach to Improving Reliability of Parallel Graph Computation. | Jin Cui, Zhenhua Duan |
| 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 | AAIM | Three Algorithms for Converting Control Flow Statements from Python to XD-M. | Jiarui Wang, Nan Zhang, Zhenhua Duan |
| 2021 | AAIM | Design and Implementation of List and Dictionary in XD-M Language. | Yajie Wang, Nan Zhang, Zhenhua Duan |
| 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 | COCOA | Propositional Projection Temporal Logic Specification Mining. | Nan Zhang, Xiaoshuai Yuan, Zhenhua Duan |
| 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 | COCOON | Extending MSVL with Semaphore. | Xinfeng Shu, Zhenhua Duan |
| 2016 | IJCAI | A Decision Procedure for a Fragment of Linear Time Mu-Calculus. | Yao Liu, Zhenhua Duan, 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 | LATA | Interval Temporal Logic Semantics of Box Algebra. | Hanna Klaudel, Maciej Koutny, Zhenhua Duan |
| 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 |
| 2013 | ICTAC | A Transformation from p-π to MSVL. | Ling Luo, Zhenhua Duan |
| 2013 | TASE | Integration of Linear Constraints with a Temporal Logic Programming Language. | Qian Ma, Zhenhua Duan, Mengfei Yang |
| 2012 | ICFEM | Time Constraints with Temporal Logic Programming. | Meng Han, Zhenhua Duan, Xiaobing Wang |
| 2012 | TASE | Symbolic Model Checking for Propositional Projection Temporal Logic. | Tao Pang, Zhenhua Duan, Cong Tian |
| 2011 | COCOA | Public Communication Based on Russian Cards Protocol: A Case Study. | Jia He, Zhenhua Duan |
| 2011 | COCOA | A Semantic Model for Many-Core Parallel Computing. | Nan Zhang, Zhenhua Duan |
| 2011 | COCOON | Making Abstraction-Refinement Efficient in Model Checking. | Cong Tian, Zhenhua Duan |
| 2011 | HPCC | ESHMP: A Stall-Time-Based Scheduling for Performance Heterogeneous Multicore Systems. | Pengcheng Nie, Zhenhua Duan, Bohu Huang |
| 2011 | ICFEM | Asynchronous Communication in MSVL. | Dapeng Mo, Xiaobing Wang, Zhenhua Duan |
| 2011 | TASE | Focus Game for Projection Temporal Logic. | Cong Tian, Zhenhua Duan |
| 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 |
| 2010 | TASE | Axiomatic Temporal Logic Programs Verification. | Xiaoxiao Yang, Zhenhua Duan |
| 2010 | TASE | Model Checking Rectangular Hybrid Systems with Timed Computation Tree Logic. | Haibin Zhang, Zhenhua Duan, Bohu Huang, Xiaobing Wang, Long Zhang |
| 2009 | COCOA | Generalized Russian Cards Problem. | Zhenhua Duan, Chen Yang |
| 2009 | ICCSA | Verification of Use Case with Petri Nets in Requirement Analysis. | Jinqiang Zhao, Zhenhua Duan |
| 2009 | TASE | An Efficient Algorithm for Finding Empty Space for Reconfigurable Systems. | Yan Xiao, Zhenhua Duan, Pengcheng Nie |
| 2008 | CSCWD | Semi-automatically annotating data semantics to web services using ontology mapping. | Man Zhang, Zhenhua Duan, Chenting Zhao |
| 2008 | ICFEM | A Unified Model Checking Approach with Projection Temporal Logic. | Zhenhua Duan, Cong Tian |
| 2008 | ICIW | Kapa: A File Sharing System Based on HP2P. | Bo Wang, Zhenhua Duan, Lei Wang |
| 2008 | ICSOC | From Business Process Models to Web Services Orchestration: The Case of UML 2.0 Activity Diagram to BPEL. | Man Zhang, Zhenhua Duan |
| 2008 | TAMC | Propositional Projection Temporal Logic, Bchi Automata and omega-Regular Expressions. | Cong Tian, Zhenhua Duan |
| 2008 | TAMC | Symbolic Algorithm Analysis of Rectangular Hybrid Systems. | Haibin Zhang, Zhenhua Duan |
| 2008 | TASE | A Complete Axiomatization of Propositional Projection Temporal Logic. | Zhenhua Duan, Nan Zhang |
| 2007 | CSCWD | Automating Web Service Composition for Collaborative Business Processes. | Lihui Lei, Zhenhua Duan |
| 2007 | ICDS | Incorporating Clusters into Hybrid P2P Network. | Ertao Lv, Zhenhua Duan, Jian-Jun Qi, Yang Cao, Zhuo Peng |
| 2007 | ICDS | HP2P: A Hybrid Hierarchical P2P Network. | Zhuo Peng, Zhenhua Duan, Jian-Jun Qi, Yang Cao, Ertao Lv |
| 2007 | ICFEM | Model Checking Propositional Projection Temporal Logic Based on SPIN. | Cong Tian, Zhenhua Duan |
| 2007 | SOFSEM | Operational Semantics of Framed Temporal Logic Programs. | Xiaoxiao Yang, Zhenhua Duan |
| 2007 | TAMC | Decidability of Propositional Projection Temporal Logic with Infinite Models. | Zhenhua Duan, Cong Tian |
| 2007 | TASE | An Interpreter for Framed Tempura and Its Application. | Yongtao Ma, Zhenhua Duan, Xiaobing Wang, Xiaoxiao Yang |
| 2006 | CSCWD | Semantic Matching of Web Services Based on Choreographies. | Lihui Lei, Zhenhua Duan, Bin Yu |
| 2006 | CSCWD | Semantic Matching of Web Services for Collaborative Business Processes. | Lihui Lei, Zhenhua Duan, Bin Yu |
| 2006 | ICWS | Transforming OWL-S Process Model into EDFA for Service Discovery. | Lihui Lei, Zhenhua Duan |
| 2005 | ICLP | Semantics of Framed Temporal Logic Programs. | Zhenhua Duan, Xiaoxiao Yang, Maciej Koutny |
| 1994 | LPAR | Projection in Temporal Logic Programming. | Zhenhua Duan, Maciej Koutny, Chris Holt |