Model Checking Propositional Projection Temporal Logic Based on SPIN. - Cong Tian 001; Zhenhua Duan (ICFEM, 2007)

Decidability of Propositional Projection Temporal Logic with Infinite Models. - Zhenhua Duan; Cong Tian 001 (TAMC, 2007)

A Unified Model Checking Approach with Projection Temporal Logic. - Zhenhua Duan; Cong Tian 001 (ICFEM, 2008)

Propositional Projection Temporal Logic, Bchi Automata and omega-Regular Expressions. - Cong Tian 001; Zhenhua Duan (TAMC, 2008)

A decision procedure for propositional projection temporal logic with infinite models. - Zhenhua Duan; Cong Tian 001; Li Zhang (Acta Informatica, 2008)

A note on stutter-invariant PLTL. - Cong Tian 001; Zhenhua Duan (Inf. Process. Lett., 2009)

Complexity of propositional projection temporal logic with star. - Cong Tian 001; Zhenhua Duan (Math. Struct. Comput. Sci., 2009)

A Transformation from PPTL to S1S. - Cong Tian 001; Zhenhua Duan (COCOA (2), 2010)

An Improved Decision Procedure for Propositional Projection Temporal Logic. - Zhenhua Duan; Cong Tian 001 (ICFEM, 2010)

Alternating Interval Based Temporal Logics. - Cong Tian 001; Zhenhua Duan (ICFEM, 2010)

Non-Functional Requirements Elicitation and Incorporation into Class Diagrams. - Xiaoyu Song; Zhenhua Duan; Cong Tian 001 (IIP, 2010)

An Executable Concurrent Model for OWL-S Process Models. - Zhenhua Duan; Cong Tian 001 (QSIC, 2010)

Making Abstraction-Refinement Efficient in Model Checking. - Cong Tian 001; Zhenhua Duan (COCOON, 2011)

Focus Game for Projection Temporal Logic. - Cong Tian 001; Zhenhua Duan (TASE, 2011)

Expressiveness of propositional projection temporal logic with star. - Cong Tian 001; Zhenhua Duan (Theor. Comput. Sci., 2011)

Abstract Model Checking with SOFL Hierarchy. - Cong Tian 001; Shaoying Liu; Zhenhua Duan (SOFL, 2012)

Model Checking C Programs with MSVL. - Yan Yu; Zhenhua Duan; Cong Tian 001; Mengfei Yang (SOFL, 2012)

Symbolic Model Checking for Propositional Projection Temporal Logic. - Tao Pang; Zhenhua Duan; Cong Tian 001 (TASE, 2012)

An efficient approach for abstraction-refinement in model checking. - Cong Tian 001; Zhenhua Duan; Nan Zhang 001 (Theor. Comput. Sci., 2012)

Model Checking. - Zhenhua Duan; Cong Tian 001 (Handbook of Finite State Based Models and Applications, 2012)

Some Fixed-Point Issues in PPTL. - Zhenhua Duan; Qian Ma; Cong Tian 001; Nan Zhang 001 (Theories of Programming and Formal Methods, 2013)

An Extended Strange Planet Protocol. - Jin Liu; Zhenhua Duan; Cong Tian 001 (COCOA, 2013)

Bounded Model Checking for Propositional Projection Temporal Logic. - Zhenhua Duan; Cong Tian 001; Mengfei Yang; Jia He (COCOON, 2013)

Deternimization of Büchi Automata as Partitioned Automata. - Cong Tian 001; Zhenhua Duan; Mengfei Yang (COCOON, 2013)

Simulation of CTCS-3 protocol with temporal logic programming. - Peng Zhang; Zhenhua Duan; Cong Tian 001 (CSCWD, 2013)

Translation from Workflow Nets to MSVL. - Ya Shi; Zhenhua Duan; Cong Tian 001 (ICFEM, 2013)

Detecting spurious counterexamples efficiently in abstract model checking. - Cong Tian 001; Zhenhua Duan (ICSE, 2013)

Present-Future Form of Linear Time $$ mu $$ -Calculus. - Yao Liu 010; Zhenhua Duan; Cong Tian 001; Bo Liu (SOFL+MSVL, 2013)

Integrating Separation Logic with PPTL. - Xu Lu 003; Zhenhua Duan; Cong Tian 001; Hongjin Liu (SOFL+MSVL, 2013)

Improved Net Reductions for LTL $$ setminus $$ X Model Checking. - Ya Shi; Zhenhua Duan; Cong Tian 001; Hua Yang (SOFL+MSVL, 2013)

Modeling and Verification of RBC Handover Protocol. - Kai Yang; Zhenhua Duan; Cong Tian 001 (TTSS, 2013)

Bounded Model Checking of Traffic Light Control System. - Bin Yu 008; Zhenhua Duan; Cong Tian 001 (TTSS, 2013)

A cylinder computation model for many-core parallel computing. - Nan Zhang 001; Zhenhua Duan; Cong Tian 001 (Theor. Comput. Sci., 2013)

Improved Even Order Magic Square Construction Algorithms and Their Applications. - Zhenhua Duan; Jin Liu; Jie Li; Cong Tian 001 (COCOA, 2014)

Normal Form Expressions of Propositional Projection Temporal Logic. - Zhenhua Duan; Cong Tian 001; Nan Zhang 001 (COCOON, 2014)

An Axiomatization for Cylinder Computation Model. - Nan Zhang 001; Zhenhua Duan; Cong Tian 001 (COCOON, 2014)

Simulation and verification of the virtual memory management system with MSVL. - Meng Wang 021; Zhenhua Duan; Cong Tian 001 (CSCWD, 2014)

Model Checking Rate-Monotonic Scheduler with TMSVL. - Jin Cui; Zhenhua Duan; Cong Tian 001 (ICECCS, 2014)

Extending MSVL with Function Calls. - Nan Zhang 001; Zhenhua Duan; Cong Tian 001 (ICFEM, 2014)

Towards more accurate content categorization of API discussions. - Bo Zhou 010; Xin Xia 001; David Lo 001; Cong Tian 001; Xinyu Wang 001 (ICPC, 2014)

Clustering and Partition Based Divide and Conquer for SAT Solving. - Quanrun Fan; Zhenhua Duan; Cong Tian 001; Hongwei Du 001 (MSN, 2014)

A Memory Management Mechanism for MSVL. - Kai Yang; Zhenhua Duan; Cong Tian 001 (SOFL+MSVL, 2014)

Unified Bounded Model Checking for MSVL. - Bin Yu 008; Zhenhua Duan; Cong Tian 001 (SOFL+MSVL, 2014)

An Improved Recursive Algorithm for Parity Games. - Yao Liu 010; Zhenhua Duan; Cong Tian 001 (TASE, 2014)

Buchi Determinization Made Tighter. - Cong Tian 001; Zhenhua Duan (CoRR, 2014)

Secure communications with strange planet protocol. - Cong Tian 001; Zhenhua Duan; Jin Liu (Optim. Lett., 2014)

A practical decision procedure for Propositional Projection Temporal Logic with infinite models. - Zhenhua Duan; Cong Tian 001 (Theor. Comput. Sci., 2014)

A formal proof of the deadline driven scheduler in PPTL axiomatic system. - Nan Zhang 001; Zhenhua Duan; Cong Tian 001; Ding-Zhu Du (Theor. Comput. Sci., 2014)

Making CEGAR More Efficient in Software Model Checking. - Cong Tian 001; Zhenhua Duan; Zhao Duan (IEEE Trans. Software Eng., 2014)

Symbolic Model Checking for Alternating Projection Temporal Logic. - Haiyang Wang; Zhenhua Duan; Cong Tian 001 (COCOA, 2015)

Model Checking MSVL Programs Based on Dynamic Symbolic Execution. - Zhenhua Duan; Kangkang Bu; Cong Tian 001; Nan Zhang 001 (COCOON, 2015)

Verification of a real time scheduling protocol of safety-critical systems. - Meng Wang 021; Zhenhua Duan; Cong Tian 001; Nan Zhang 001 (CSCWD, 2015)

Model Checking mu μ C/OS-III Multi-task System with TMSVL. - Jin Cui; Zhenhua Duan; Cong Tian 001; Nan Zhang 001; Conghao Zhou (ICFEM, 2015)

A Self-ORganizing Trust Model Based on HP2P. - Zhenhua Duan; Yujiang Hui; Cong Tian 001; Nan Zhang 001; Bohu Huang (MSN, 2015)

Modeling and Verification of an Interrupt System in mu μ C/OS-III with TMSVL. - Jin Cui; Zhenhua Duan; Cong Tian 001; Nan Zhang 001 (SOFL+MSVL, 2015)

LtlNfBa: Making LTL Translation More Practical. - Cong Tian 001; Jun Song; Zhenhua Duan; Zhao Duan (SOFL+MSVL, 2015)

PPTL_SPIN: A SPIN Based Model Checker for Propositional Projection Temporal Logic. - Xiaoming Zhang; Zhenhua Duan; Cong Tian 001 (SOFL+MSVL, 2015)

An Improved Decision Procedure for Linear Time Mu-Calculus. - Yao Liu 010; Zhenhua Duan; Cong Tian 001 (CoRR, 2015)

Extending PPTL for Verifying Heap Evolution Properties. - Xu Lu 003; Zhenhua Duan; Cong Tian 001 (CoRR, 2015)

An extended strange planet protocol. - Jin Liu; Zhenhua Duan; Cong Tian 001; Nan Zhang 001 (J. Comb. Optim., 2015)

A structural transformation from p-π to MSVL. - Ling Luo; Zhenhua Duan; Cong Tian 001; Xiaobing Wang (J. Comb. Optim., 2015)

Transformation from PLTL to automata via NFGs. - Cong Tian 001; Zhenhua Duan; Mengfei Yang (J. Comb. Optim., 2015)

Improved even order magic square construction algorithms and their applications in multi-user shared electronic accounts. - Zhenhua Duan; Jin Liu; Jie Li; Cong Tian 001 (Theor. Comput. Sci., 2015)

Verifying OSEK/VDX applications: An optimized SMT-based bounded model checking approach. - Haitao Zhang; Zhuo Cheng; Cong Tian 001; Yonggang Lu; Guoqiang Li 001 (ICIS, 2016)

Using Unified Model Checking to Verify Heaps. - Xu Lu 003; Zhenhua Duan; Cong Tian 001 (COCOA, 2016)

Satisfiability of Linear Time Mu-Calculus on Finite Traces. - Yao Liu 010; Zhenhua Duan; Cong Tian 001; Bin Cui 001 (COCOON, 2016)

A Decision Procedure for a Fragment of Linear Time Mu-Calculus. - Yao Liu 010; Zhenhua Duan; Cong Tian 001 (IJCAI, 2016)

How android app developers manage power consumption?: an empirical study by mining power management commits. - Lingfeng Bao; David Lo 001; Xin Xia 001; Xinyu Wang 001; Cong Tian 001 (MSR, 2016)

A Proof System for MSVL Programs in Coq. - Lin Qian; Zhenhua Duan; Nan Zhang 001; Cong Tian 001 (SOFL+MSVL, 2016)

Model checking concurrent systems with MSVL. - Nan Zhang 001; Zhenhua Duan; Cong Tian 001 (Sci. China Inf. Sci., 2016)

Model checking Petri nets with MSVL. - Ya Shi; Cong Tian 001; Zhenhua Duan; Mengchu Zhou (Inf. Sci., 2016)

Verifying safety critical task scheduling systems in PPTL axiom system. - Nan Zhang 001; Mengfei Yang; Bin Gu 006; Zhenhua Duan; Cong Tian 001 (J. Comb. Optim., 2016)

A canonical form based decision procedure and model checking approach for propositional projection temporal logic. - Zhenhua Duan; Cong Tian 001; Nan Zhang 001 (Theor. Comput. Sci., 2016)

A complete axiom system for propositional projection temporal logic with cylinder computation model. - Nan Zhang 001; Zhenhua Duan; Cong Tian 001 (Theor. Comput. Sci., 2016)

A mechanism of function calls in MSVL. - Nan Zhang 001; Zhenhua Duan; Cong Tian 001 (Theor. Comput. Sci., 2016)

Modeling and Verifying Multi-core Programs. - Nan Zhang 001; Zhenhua Duan; Cong Tian 001; Hongwei Du 001; Kai Yang (COCOA (2), 2017)

Cloning Automata: Simulation and Analysis of Computer Bacteria. - Chu Chen; Zhenhua Duan; Cong Tian 001; Hongwei Du 001 (COCOA (1), 2017)

Verifying Temporal Properties of C Programs via Lazy Abstraction. - Zhao Duan; Cong Tian 001; Zhenhua Duan (ICFEM, 2017)

Full regular temporal property verification as dynamic program execution. - Meng Wang 021; Cong Tian 001; Zhenhua Duan (ICSE (Companion Volume), 2017)

Temporalising Separation Logic for Planning with Search Control Knowledge. - Xu Lu 003; Cong Tian 001; Zhenhua Duan (IJCAI, 2017)

More effective interpolations in software model checking. - Cong Tian 001; Zhao Duan; Zhenhua Duan; C.-H. Luke Ong (ASE, 2017)

Implementing MapReduce with MSVL. - Nan Zhang 001; Meng Wang 021; Zhenhua Duan; Cong Tian 001; Jin Cui (SOFL+MSVL, 2017)

Model Checking Multi-agent Systems with APTL. - Haiyang Wang; Zhenhua Duan; Cong Tian 001 (Ad Hoc Sens. Wirel. Networks, 2017)

MSVL: a typed language for temporal logic programming. - Xiaobing Wang; Cong Tian 001; Zhenhua Duan; Liang Zhao 021 (Frontiers Comput. Sci., 2017)

Two-layer hybrid peer-to-peer networks. - Zhenhua Duan; Cong Tian 001; Mengchu Zhou; Xiaobing Wang; Nan Zhang 001; Hongwei Du 001; Lei Wang 126 (Peer-to-Peer Netw. Appl., 2017)

A Novel Approach to Verifying Context Free Properties of Programs. - Nan Zhang 001; Zhenhua Duan; Cong Tian 001; Hongwei Du 001 (AAIM, 2018)

Reducing Extension Edges of Concurrent Programs for Reachability Analysis. - Cong Tian 001; Jiaying Wang; Zhenhua Duan; Liang Zhao 021 (COCOA, 2018)

RFC-directed differential testing of certificate validation in SSL/TLS implementations. - Chu Chen; Cong Tian 001; Zhenhua Duan; Liang Zhao 021 (ICSE, 2018)

Accelerating counterexample detection in software model checking. - Cong Tian 001; Zhao Duan; Zhenhua Duan (ICSE (Companion Volume), 2018)

Android inter-component communication analysis with intent revision. - Cong Tian 001; Congli Xia; Zhenhua Duan (ICSE (Companion Volume), 2018)

A Blockchain Implementation of an Attendance Management System. - Jingyao Tu; Zhenhua Duan; Cong Tian 001; Nan Zhang 001; Ying Wu (SOFL+MSVL, 2018)

InterpChecker: Reducing State Space via Interpolations - (Competition Contribution). - Zhao Duan; Cong Tian 001; Zhenhua Duan; C.-H. Luke Ong (TACAS (2), 2018)

Translating C programs to MSVL programs. - Meng Wang 021; Cong Tian 001; Nan Zhang 001; Zhenhua Duan; Chenguang Yao (CoRR, 2018)

On general threshold and general cascade models of social influence. - Weili Wu 001; Hongwei Du 001; Huijuan Wang; Lidong Wu; Zhenhua Duan; Cong Tian 001 (J. Comb. Optim., 2018)

Verifying temporal properties of programs: A parallel approach. - Bin Yu 008; Zhenhua Duan; Cong Tian 001; Nan Zhang 001 (J. Parallel Distributed Comput., 2018)

A Runtime Optimization Approach for FPGA Routing. - Dekui Wang; Zhenhua Duan; Cong Tian 001; Bohu Huang; Nan Zhang 001 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2018)

A compiler for MSVL and its applications. - Kai Yang; Zhenhua Duan; Cong Tian 001; Nan Zhang 001 (Theor. Comput. Sci., 2018)

Planning with Spatio-Temporal Search Control Knowledge. - Xu Lu 003; Cong Tian 001; Zhenhua Duan; Hongwei Du 001 (IEEE Trans. Knowl. Data Eng., 2018)

A Novel Approach to Modeling and Verifying Real-Time Systems for High Reliability. - Jin Cui; Zhenhua Duan; Cong Tian 001; Hongwei Du 001 (IEEE Trans. Reliab., 2018)

FastDroid: efficient taint analysis for Android applications. - Jie Zhang 084; Cong Tian 001; Zhenhua Duan (ICSE (Companion Volume), 2019)

Verifying schedulability of tasks in ROS-based systems. - Jin Cui; Cong Tian 001; Nan Zhang 001; Zhenhua Duan; Hongwei Du 001 (J. Comb. Optim., 2019)

Verifying a scheduling protocol of safety-critical systems. - Meng Wang 021; Cong Tian 001; Nan Zhang 001; Zhenhua Duan; Hongwei Du 001 (J. Comb. Optim., 2019)

A temporal logic programming approach to planning. - Kai Yang; Cong Tian 001; Nan Zhang 001; Zhenhua Duan; Hongwei Du 001 (J. Comb. Optim., 2019)

Index set expressions can represent temporal logic formulas. - Zhenhua Duan; Cong Tian 001; Nan Zhang 001; Qian Ma; Hongwei Du 001 (Theor. Comput. Sci., 2019)

Model checking open systems with alternating projection temporal logic. - Cong Tian 001; Zhenhua Duan (Theor. Comput. Sci., 2019)

Differential Testing of Certificate Validation in SSL/TLS Implementations: An RFC-guided Approach. - Cong Tian 001; Chu Chen; Zhenhua Duan; Liang Zhao 021 (ACM Trans. Softw. Eng. Methodol., 2019)

Verifying Full Regular Temporal Properties of Programs via Dynamic Program Execution. - Meng Wang 021; Cong Tian 001; Nan Zhang 001; Zhenhua Duan (IEEE Trans. Reliab., 2019)

Transforming Multi-matching Nested Traceable Automata to Multi-matching Nested Expressions. - Jin Liu; Zhenhua Duan; Cong Tian 001 (COCOA, 2020)

Distilling Knowledge in Adversarial Attack. - Zeqian Dong; Long Tang; Cong Tian 001 (DSA, 2020)

Making Streett Determinization Tight. - Cong Tian 001; Wensheng Wang; Zhenhua Duan (LICS, 2020)

RTPDroid: Detecting Implicitly Malicious Behaviors Under Runtime Permission Model. - Jie Zhang 084; Cong Tian 001; Zhenhua Duan; Liang Zhao 021 (QRS, 2020)

Generating Adversarial Examples withControllable Non-transferability. - Renzhi Wang; Tianwei Zhang 004; Xiaofei Xie; Lei Ma 003; Cong Tian 001; Felix Juefei-Xu; Yang Liu 003 (CoRR, 2020)

P2P Network Based Smart Parking System Using Edge Computing. - Nan Zhang 001; Xu Lu 003; Cong Tian 001; Zhenhua Duan; Zhifeng Sun; Ting Zhang (Mob. Networks Appl., 2020)

ParRA: A Shared Memory Parallel FPGA Router Using Hybrid Partitioning Approach. - Dekui Wang; Zhenhua Duan; Cong Tian 001; Bohu Huang; Nan Zhang 001 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020)

Verify heaps via unified model checking. - Xu Lu 003; Zhenhua Duan; Cong Tian 001; Hongwei Du 001 (Theor. Comput. Sci., 2020)

Translating Xd-C programs to MSVL programs. - Meng Wang 021; Cong Tian 001; Nan Zhang 001; Zhenhua Duan; Chenguang Yao (Theor. Comput. Sci., 2020)

Malware Detection using CNN via Word Embedding. - Jie Zhang 084; Lin Yan; Rong Wang; Cong Tian 001; Zhenhua Duan (DSA, 2021)

Improving Quality of Counterexamples in Model Checking via Automated Planning. - Xu Lu 003; Cong Tian 001; Bin Yu 008; Zhenhua Duan (QRS, 2021)

Conditional interpolation: making concurrent program verification more effective. - Jie Su 002; Cong Tian 001; Zhenhua Duan (ESEC/SIGSOFT FSE, 2021)

An efficient approach for taint analysis of android applications. - Jie Zhang 084; Cong Tian 001; Zhenhua Duan (Comput. Secur., 2021)

Preface to the Topic of Formal Methods and Their Applications. - Cong Tian 001; Yuxin Deng; Yu Jiang (Int. J. Softw. Informatics, 2021)

A dynamic approach to detecting, eliminating and fixing memory leaks. - Bin Yu 008; Cong Tian 001; Nan Zhang 001; Zhenhua Duan; Hongwei Du 001 (J. Comb. Optim., 2021)

Malware Detection Using CNN via Word Embedding in Cloud Computing Infrastructure. - Rong Wang; Cong Tian 001; Lin Yan (Sci. Program., 2021)

Multi-matching nested relations. - Jin Liu; Zhenhua Duan; Cong Tian 001 (Theor. Comput. Sci., 2021)

Unified temporal logic. - Nan Zhang 001; Zhenhua Duan; Cong Tian 001 (Theor. Comput. Sci., 2021)

Temporal logic specification mining of programs. - Nan Zhang 001; Bin Yu 008; Cong Tian 001; Zhenhua Duan; Xiaoshuai Yuan (Theor. Comput. Sci., 2021)

A Knowledge-Based Temporal Planning Approach for Urban Traffic Control. - Xu Lu 003; Nan Zhang 001; Cong Tian 001; Bin Yu 008; Zhenhua Duan (IEEE Trans. Intell. Transp. Syst., 2021)

A CEGAR-Based Static-Dynamic Approach to Verifying Full Regular Properties of C Programs. - Kai Yang; Cong Tian 001; Nan Zhang 001; Zhenhua Duan; Hongwei Du 001 (IEEE Trans. Reliab., 2021)

Prioritized Constraint-Aided Dynamic Partial-Order Reduction. - Jie Su 002; Cong Tian 001; Zuchao Yang; Jiyu Yang; Bin Yu 008; Zhenhua Duan (ASE, 2022)

An Empirical Study on Software Defect Prediction using Function Point Analysis. - Xinghan Zhao; Cong Tian 001 (QRS, 2022)

Inferring Exact Domains to Efficiently Generate Valid Test Cases via Testing. - Chu Chen; Xuan Wang; Pinghong Ren; Zhenhua Duan; Cong Tian 001; Xu Lu 003; Bin Yu 008 (SOFL+MSVL, 2022)

Formulate Full View Camera Sensor Coverage by Using Group Set Coverage. - Hongwei Du 001; Zhao Zhang 002; Zhenhua Duan; Cong Tian 001; Ding-Zhu Du (WiCON, 2022)

Improving transferability of adversarial examples by saliency distribution and data augmentation. - Yansong Dong; Long Tang; Cong Tian 001; Bin Yu 008; Zhenhua Duan (Comput. Secur., 2022)

A novel load balancing scheme for mobile edge computing. - Zhenhua Duan; Cong Tian 001; Nan Zhang 001; Mengchu Zhou; Bin Yu 008; Xiaobing Wang; Jiangen Guo; Ying Wu (J. Syst. Softw., 2022)

PPTL specification mining based on LNFG. - Xinya Ning; Nan Zhang 001; Zhenhua Duan; Cong Tian 001 (Theor. Comput. Sci., 2022)

Verifying Properties of MapReduce-Based Big Data Processing. - Nan Zhang 001; Meng Wang 021; Zhenhua Duan; Cong Tian 001 (IEEE Trans. Reliab., 2022)

PIChecker for SV-COMP 2023. - Jie Su 002; Zuchao Yang; Hengrui Xing; Jiyu Yang; Cong Tian 001; Zhenhua Duan (Zenodo, 2022)

A Dynamic Parameter Adaptive Path Planning Algorithm. - Guangyu Yao; Nan Zhang 001; Zhenhua Duan; Cong Tian 001 (COCOA (2), 2023)

An Approach to Agent Path Planning Under Temporal Logic Constraints. - Chaofeng Yu; Nan Zhang 001; Zhenhua Duan; Cong Tian 001 (COCOON (2), 2023)

SBDT: Search-Based Differential Testing of Certificate Parsers in SSL/TLS Implementations. - Chu Chen; Pinghong Ren; Zhenhua Duan; Cong Tian 001; Xu Lu 003; Bin Yu 008 (ISSTA, 2023)

Adversarial Training of Deep Neural Networks Guided by Texture and Structural Information. - Zhaoxin Wang; Handing Wang; Cong Tian 001; Yaochu Jin (ACM Multimedia, 2023)

Detecting Atomicity Violations in Interrupt-Driven Programs via Interruption Points Selecting and Delayed ISR-Triggering. - Bin Yu 008; Cong Tian 001; Hengrui Xing; Zuchao Yang; Jie Su 002; Xu Lu 003; Jiyu Yang; Liang Zhao 021; Xiaofeng Li; Zhenhua Duan (ESEC/SIGSOFT FSE, 2023)

PIChecker: A POR and Interpolation based Verifier for Concurrent Programs (Competition Contribution). - Jie Su 002; Zuchao Yang; Hengrui Xing; Jiyu Yang; Cong Tian 001; Zhenhua Duan (TACAS (2), 2023)

Verifying Chips Design at RTL Level. - Wu Wang; Nan Zhang 001; Cong Tian 001; Zhenhua Duan; Zhijie Xu; Chaofeng Yu (TASE, 2023)

Automatic Identification of Crash-inducing Smart Contracts. - Chao Ni 001; Cong Tian 001; Kaiwen Yang; David Lo 001; Jiachi Chen; Xiaohu Yang 001 (SANER, 2023)

Using Experience Classification for Training Non-Markovian Tasks. - Ruixuan Miao; Xu Lu 003; Cong Tian 001; Bin Yu 008; Zhenhua Duan (CoRR, 2023)

A variational Bayesian approach for partly resolvable group tracking. - Zhenzhen Su; Long Liu 004; Hongbing Ji; Cong Tian 001 (Signal Process., 2023)

A Distributed Network-Based Runtime Verification of Full Regular Temporal Properties. - Bin Yu 008; Cong Tian 001; Xu Lu 003; Nan Zhang 001; Zhenhua Duan (IEEE Trans. Parallel Distributed Syst., 2023)

A proof system for unified temporal logic. - Nan Zhang 001; Chaofeng Yu; Zhenhua Duan; Cong Tian 001 (Theor. Comput. Sci., 2023)

Adaptively parallel runtime verification based on distributed network for temporal properties. - Bin Yu 008; Xu Lu 003; Cong Tian 001; Meng Wang 021; Chu Chen; Ming Lei 003; Zhenhua Duan (Parallel Comput., 2023)

Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification. - Cheng Wen 002; Jialun Cao; Jie Su 002; Zhiwu Xu 001; Shengchao Qin; Mengda He; Haokun Li; Shing-Chi Cheung; Cong Tian 001 (CAV (2), 2024)

DACPara: A Divide-and-Conquer Parallel Approach for High-Quality Logic Rewriting in Large-Scale Circuits. - Nanjiang Qu; Cong Tian 001; Zhenhua Duan (DAC, 2024)

Preventing Catastrophic Overfitting in Fast Adversarial Training: A Bi-level Optimization Perspective. - Zhaoxin Wang; Handing Wang; Cong Tian 001; Yaochu Jin (ECCV (28), 2024)

DynaEDI: Decentralized Integrity Verification for Dynamic Edge Data. - Qiang He 001; Jiyu Yang; Feifei Chen 001; Cong Tian 001; Yanhui Li; Yun Yang 001 (ICSOC (1), 2024)

Detecting Atomicity Violations for Interrupt-driven Programs via Systematic Scheduling and Prefix-directed Feedback. - Ruixue Li; Bin Yu 008; Xu Lu 003; Lei Ke; Jiawei Chen; Zixuan Yuan; Jingxian Wang; Cong Tian 001; Yansong Dong (ASE, 2024)

A Contract-Based Framework for Formal Verification of Embedded Software. - Xu Lu 003; Cong Tian 001; Bin Gu 006; Bin Yu 008; Chen Chen; Zhenhua Duan (SETTA, 2024)

CFStra: Enhancing Configurable Program Analysis Through LLM-Driven Strategy Selection Based on Code Features. - Jie Su 002; Liansai Deng; Cheng Wen 002; Shengchao Qin; Cong Tian 001 (TASE, 2024)

Towards Practical Requirement Analysis and Verification: A Case Study on Software IP Components in Aerospace Embedded Systems. - Zhi Ma; Cheng Wen 002; Jie Su 002; Ming Zhao; Bin Yu 008; Xu Lu 003; Cong Tian 001 (CoRR, 2024)

ParMod: A Parallel and Modular Framework for Learning Non-Markovian Tasks. - Ruixuan Miao; Xu Lu 003; Cong Tian 001; Bin Yu 008; Zhenhua Duan (CoRR, 2024)

Using experience classification for training non-Markovian tasks. - Ruixuan Miao; Xu Lu 003; Cong Tian 001; Bin Yu 008; Jin Cui; Zhenhua Duan (Expert Syst. Appl., 2024)

Efficient adversarial training with multi-fidelity optimization for robust neural network. - Zhaoxin Wang; Handing Wang; Cong Tian 001; Yaochu Jin (Neurocomputing, 2024)

Multi-keyword ranked search with access control for multiple data owners in the cloud. - Jiaqi Guo; Cong Tian 001; Xu Lu 003; Liang Zhao 021; Zhenhua Duan (J. Inf. Secur. Appl., 2024)

Verifiable privacy-preserving semantic retrieval scheme in the edge computing. - Jiaqi Guo; Cong Tian 001; Qiang He 001; Liang Zhao 021; Zhenhua Duan (J. Syst. Archit., 2024)

Intermediate-grained kernel elements pruning with structured sparsity. - Peng Zhang; Liang Zhao 021; Cong Tian 001; Zhenhua Duan (Neural Networks, 2024)

Neuron importance based verification of neural networks via divide and conquer. - Yansong Dong; Yuehao Liu; Liang Zhao 021; Cong Tian 001; Zhenhua Duan (Neurocomputing, 2024)

A multi-granularity CNN pruning framework via deformable soft mask with joint training. - Peng Zhang; Cong Tian 001; Liang Zhao 021; Zhenhua Duan (Neurocomputing, 2024)

Full View Maximum Coverage of Camera Sensors: Moving Object Monitoring. - Hongwei Du 001; Jingfang Su; Zhao Zhang 002; Zhenhua Duan; Cong Tian 001; Ding-Zhu Du (ACM Trans. Sens. Networks, 2024)

Automatically Inspecting Thousands of Static Bug Warnings with Large Language Model: How Far Are We? - Cheng Wen 002; Yuandao Cai; Bin Zhang; Jie Su 002; Zhiwu Xu 001; Dugang Liu; Shengchao Qin; Zhong Ming 001; Cong Tian 001 (ACM Trans. Knowl. Discov. Data, 2024)

From Informal to Formal - Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs. - Jialun Cao; Yaojie Lu 001; Meiziniu Li; Haoyang Ma; Haokun Li; Mengda He; Cheng Wen 002; Le Sun 001; Hongyu Zhang 002; Shengchao Qin; Shing-Chi Cheung; Cong Tian 001 (ACL (1), 2025)

CoopKG: An Academic Knowledge Graph for Question Answering Systems. - Muyuan Niu; Cong Tian 001 (DASFAA (2), 2025)

Neuron Similarity-Based Neural Network Verification via Abstraction and Refinement. - Yuehao Liu; Yansong Dong; Liang Zhao 021; Wensheng Wang; Cong Tian 001 (IJCAI, 2025)

Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision. - Xu Lu 003; Weisong Sun; Yiran Zhang; Ming Hu 003; Cong Tian 001; Zhi Jin 001; Yang Liu 003 (ASE, 2025)

Bridging Natural Language and Formal Specification-Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs. - Zhi Ma; Cheng Wen 002; Zhexin Su; Xiao Liang; Cong Tian 001; Shengchao Qin; Mengfei Yang (ASE, 2025)

EdgeThemis: Ensuring Model Integrity for Edge Intelligence. - Jiyu Yang; Qiang He 001; Zheyu Zhou; Xiaohai Dai; Feifei Chen 001; Cong Tian 001; Yun Yang 001 (WWW, 2025)

On the exploitation of control knowledge for enhancing automated planning. - Xu Lu 003; Bin Yu 008; Cong Tian 001; Chu Chen; Zhenhua Duan (Inf. Sci., 2025)

Intra-head pruning for vision transformers via inter-layer dimension relationship modeling. - Peng Zhang; Cong Tian 001; Liang Zhao 021; Zhenhua Duan (Neural Networks, 2025)

Verifying chip designs at RTL level. - Nan Zhang 001; Zhijie Xu; Zhenhua Duan; Cong Tian 001; Wu Wang; Chaofeng Yu (Sci. Comput. Program., 2025)

SAT-based bounded model checking for propositional projection temporal logic. - Zhenhua Duan; Cong Tian 001; Nan Zhang 001; Chaofeng Yu; Mengfei Yang; Jia He (Theor. Comput. Sci., 2025)

Improved SARSA and DQN algorithms for reinforcement learning. - Guangyu Yao; Nan Zhang 001; Zhenhua Duan; Cong Tian 001 (Theor. Comput. Sci., 2025)

DynaEDI+: Reliable and Decentralized Integrity Verification for Dynamic Edge Data. - Jiyu Yang; Qiang He 001; Guobiao Zhang; Feifei Chen 001; Cong Tian 001; Yun Yang 001 (IEEE Trans. Serv. Comput., 2025)

AutoTestForge: A Multidimensional Automated Testing Framework for Natural Language Processing Models. - Hengrui Xing; Cong Tian 001; Liang Zhao 021; Zhi Ma; Wensheng Wang; Nan Zhang 001; Chao Huang; Zhenhua Duan (CoRR, 2025)

Token-Level Constraint Boundary Search for Jailbreaking Text-to-Image Models. - Jiangtao Liu; Zhaoxin Wang; Handing Wang; Cong Tian 001; Yaochu Jin (CoRR, 2025)

Implicit Jailbreak Attacks via Cross-Modal Information Concealment on Vision-Language Models. - Zhaoxin Wang; Handing Wang; Cong Tian 001; Yaochu Jin (CoRR, 2025)

Inference performance evaluation for LLMs on edge devices with a novel benchmarking framework and metric. - Hao Chen; Cong Tian 001; Zixuan He; Bin Yu 008; Yepang Liu 001; Jialun Cao (CoRR, 2025)

Enhancing the Effectiveness and Durability of Backdoor Attacks in Federated Learning through Maximizing Task Distinction. - Zhaoxin Wang; Handing Wang; Cong Tian 001; Yaochu Jin (CoRR, 2025)

T4NMTD: Transition-Centric Reinforcement Learning for Non-Markovian Task Decomposition. - Ruixuan Miao; Xu Lu 003; Cong Tian 001; Bin Yu 008; Zhenhua Duan (AAAI, 2026)

Automated LTL Specification Generation from Industrial Aerospace Requirements. - Zhi Ma; Xiao Liang; Cheng Wen 002; Rui Chen 042; Bin Gu 006; Shengchao Qin; Cong Tian 001; Mengfei Yang (FM (2), 2026)

LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation. - Dong Xu; Jialun Cao; Guozhao Mo; Junjie Hu; Cheng Wen 002; Hongyu Lin; Xianpei Han; Shengchao Qin; Cong Tian 001; Shing-Chi Cheung; Le Sun 001; Yaojie Lu 001 (CoRR, 2026)