Zhenhua Duan - RankMe

243 papers A* 9A 3B 3C 42Misc 22Journal 98Unranked 53

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Engineering application of non-dominated sorting genetic algorithm III: Multi-objective optimization of ultra-high performance concrete for diverse scenarios. Eng. Appl. Artif. Intell. Wei Zhang, Zhenhua Duan, Yuqing Wu, Chao Liu, Yizhou Yao, Ahmed Nasr, Qingmei Yang, Huiyu Xia
2026	A*	`conf`	T4NMTD: Transition-Centric Reinforcement Learning for Non-Markovian Task Decomposition. AAAI Ruixuan Miao, Xu Lu, Cong Tian, Bin Yu, Zhenhua Duan
2025	J	`jnl`	AutoTestForge: A Multidimensional Automated Testing Framework for Natural Language Processing Models. CoRR Hengrui Xing, Cong Tian, Liang Zhao, Zhi Ma, Wensheng Wang, Nan Zhang, Chao Huang, Zhenhua Duan
2025	J	`jnl`	Collaboration with Generative AI to improve Requirements Change. Comput. Stand. Interfaces Yuan Kong, Nan Zhang, Zhenhua Duan, Bin Yu
2025	—	`conf`	From Line Sketches to Contextualized Scenes: An AR Scaffold for Narrative Drawing Based on Sketch Recognition and Its Motivational Effects. VRCAI Zhian Chen, Zhenhua Duan, Yunxiang Qi, Wenxiao Wang
2025	J	`jnl`	Improved SARSA and DQN algorithms for reinforcement learning. Theor. Comput. Sci. Guangyu Yao, Nan Zhang, Zhenhua Duan, Cong Tian
2025	—	`conf`	Improving Origami Instruction through Augmented Reality: A Case Study in 3D-Visualized Tutorials. VRCAI Yunxiang Qi, Zhian Chen, Zhenhua Duan, Wenxiao Wang
2025	J	`jnl`	Intra-head pruning for vision transformers via inter-layer dimension relationship modeling. Neural Networks Peng Zhang, Cong Tian, Liang Zhao, Zhenhua Duan
2025	J	`jnl`	On the exploitation of control knowledge for enhancing automated planning. Inf. Sci. Xu Lu, Bin Yu, Cong Tian, Chu Chen, Zhenhua Duan
2025	J	`jnl`	SAT-based bounded model checking for propositional projection temporal logic. Theor. Comput. Sci. Zhenhua Duan, Cong Tian, Nan Zhang, Chaofeng Yu, Mengfei Yang, Jia He
2025	J	`jnl`	Verifying chip designs at RTL level. Sci. Comput. Program. Nan Zhang, Zhijie Xu, Zhenhua Duan, Cong Tian, Wu Wang, Chaofeng Yu
2024	Misc	`conf`	A Contract-Based Framework for Formal Verification of Embedded Software. SETTA Xu Lu, Cong Tian, Bin Gu, Bin Yu, Chen Chen, Zhenhua Duan
2024	J	`jnl`	A multi-granularity CNN pruning framework via deformable soft mask with joint training. Neurocomputing Peng Zhang, Cong Tian, Liang Zhao, Zhenhua Duan
2024	Misc	`conf`	An Approach to Improving Reliability of Parallel Graph Computation. TASE Jin Cui, Zhenhua Duan
2024	A*	`conf`	DACPara: A Divide-and-Conquer Parallel Approach for High-Quality Logic Rewriting in Large-Scale Circuits. DAC Nanjiang Qu, Cong Tian, Zhenhua Duan
2024	J	`jnl`	Full View Maximum Coverage of Camera Sensors: Moving Object Monitoring. ACM Trans. Sens. Networks Hongwei Du, Jingfang Su, Zhao Zhang, Zhenhua Duan, Cong Tian, Ding-Zhu Du
2024	J	`jnl`	Generating Java code pairing with ChatGPT. Theor. Comput. Sci. Zelong Zhao, Nan Zhang, Bin Yu, Zhenhua Duan
2024	J	`jnl`	Intermediate-grained kernel elements pruning with structured sparsity. Neural Networks Peng Zhang, Liang Zhao, Cong Tian, Zhenhua Duan
2024	J	`jnl`	Multi-keyword ranked search with access control for multiple data owners in the cloud. J. Inf. Secur. Appl. Jiaqi Guo, Cong Tian, Xu Lu, Liang Zhao, Zhenhua Duan
2024	J	`jnl`	Neuron importance based verification of neural networks via divide and conquer. Neurocomputing Yansong Dong, Yuehao Liu, Liang Zhao, Cong Tian, Zhenhua Duan
2024	J	`jnl`	ParMod: A Parallel and Modular Framework for Learning Non-Markovian Tasks. CoRR Ruixuan Miao, Xu Lu, Cong Tian, Bin Yu, Zhenhua Duan
2024	J	`jnl`	Using experience classification for training non-Markovian tasks. Expert Syst. Appl. Ruixuan Miao, Xu Lu, Cong Tian, Bin Yu, Jin Cui, Zhenhua Duan
2024	J	`jnl`	Verifiable privacy-preserving semantic retrieval scheme in the edge computing. J. Syst. Archit. Jiaqi Guo, Cong Tian, Qiang He, Liang Zhao, Zhenhua Duan
2023	J	`jnl`	A Distributed Network-Based Runtime Verification of Full Regular Temporal Properties. IEEE Trans. Parallel Distributed Syst. Bin Yu, Cong Tian, Xu Lu, Nan Zhang, Zhenhua Duan
2023	—	`conf`	A Dynamic Parameter Adaptive Path Planning Algorithm. COCOA (2) Guangyu Yao, Nan Zhang, Zhenhua Duan, Cong Tian
2023	J	`jnl`	A proof system for unified temporal logic. Theor. Comput. Sci. Nan Zhang, Chaofeng Yu, Zhenhua Duan, Cong Tian
2023	J	`jnl`	Adaptively parallel runtime verification based on distributed network for temporal properties. Parallel Comput. Bin Yu, Xu Lu, Cong Tian, Meng Wang, Chu Chen, Ming Lei, Zhenhua Duan
2023	—	`conf`	An Approach to Agent Path Planning Under Temporal Logic Constraints. COCOON (2) Chaofeng Yu, Nan Zhang, Zhenhua Duan, Cong Tian
2023	—	`conf`	Detecting Atomicity Violations in Interrupt-Driven Programs via Interruption Points Selecting and Delayed ISR-Triggering. ESEC/SIGSOFT FSE Bin Yu, Cong Tian, Hengrui Xing, Zuchao Yang, Jie Su, Xu Lu, Jiyu Yang, Liang Zhao, Xiaofeng Li, Zhenhua Duan
2023	—	`conf`	PIChecker: A POR and Interpolation based Verifier for Concurrent Programs (Competition Contribution). TACAS (2) Jie Su, Zuchao Yang, Hengrui Xing, Jiyu Yang, Cong Tian, Zhenhua Duan
2023	A	`conf`	SBDT: Search-Based Differential Testing of Certificate Parsers in SSL/TLS Implementations. ISSTA Chu Chen, Pinghong Ren, Zhenhua Duan, Cong Tian, Xu Lu, Bin Yu
2023	—	`ed.`	Structured Object-Oriented Formal Language and Method - 11th International Workshop, SOFL+MSVL 2022, Madrid, Spain, October 24, 2022, Revised Selected Papers SOFL+MSVL Shaoying Liu, Zhenhua Duan, Ai Liu
2023	J	`jnl`	Using Experience Classification for Training Non-Markovian Tasks. CoRR Ruixuan Miao, Xu Lu, Cong Tian, Bin Yu, Zhenhua Duan
2023	Misc	`conf`	Verifying Chips Design at RTL Level. TASE Wu Wang, Nan Zhang, Cong Tian, Zhenhua Duan, Zhijie Xu, Chaofeng Yu
2022	J	`jnl`	A novel load balancing scheme for mobile edge computing. J. Syst. Softw. Zhenhua Duan, Cong Tian, Nan Zhang, MengChu Zhou, Bin Yu, Xiaobing Wang, Jiangen Guo, Ying Wu
2022	—	`conf`	An Approach for Automatically Generating Traces for Python Programs. DSA Xiaoting Zhong, Nan Zhang, Zhenhua Duan
2022	—	`conf`	Formulate Full View Camera Sensor Coverage by Using Group Set Coverage. WiCON Hongwei Du, Zhao Zhang, Zhenhua Duan, Cong Tian, Ding-Zhu Du
2022	—	`conf`	Implementation of Matlab matfun Toolkit Based on MSVL. SOFL+MSVL Xueqing Feng, Nan Zhang, Zhenhua Duan
2022	J	`jnl`	Improving transferability of adversarial examples by saliency distribution and data augmentation. Comput. Secur. Yansong Dong, Long Tang, Cong Tian, Bin Yu, Zhenhua Duan
2022	—	`conf`	Inferring Exact Domains to Efficiently Generate Valid Test Cases via Testing. SOFL+MSVL Chu Chen, Xuan Wang, Pinghong Ren, Zhenhua Duan, Cong Tian, Xu Lu, Bin Yu
2022	J	`jnl`	PPTL specification mining based on LNFG. Theor. Comput. Sci. Xinya Ning, Nan Zhang, Zhenhua Duan, Cong Tian
2022	A*	`conf`	Prioritized Constraint-Aided Dynamic Partial-Order Reduction. ASE Jie Su, Cong Tian, Zuchao Yang, Jiyu Yang, Bin Yu, Zhenhua Duan
2022	C	`conf`	Three Algorithms for Converting Control Flow Statements from Python to XD-M. AAIM Jiarui Wang, Nan Zhang, Zhenhua Duan
2022	—	`conf`	USV Path Planning Based on Adaptive Fuzzy Reward. IJCRS Zhenhua Duan, Guoyin Wang, Qun Liu, Yan Shi
2022	J	`jnl`	Verifying Properties of MapReduce-Based Big Data Processing. IEEE Trans. Reliab. Nan Zhang, Meng Wang, Zhenhua Duan, Cong Tian
2021	J	`jnl`	A CEGAR-Based Static-Dynamic Approach to Verifying Full Regular Properties of C Programs. IEEE Trans. Reliab. Kai Yang, Cong Tian, Nan Zhang, Zhenhua Duan, Hongwei Du
2021	J	`jnl`	A Knowledge-Based Temporal Planning Approach for Urban Traffic Control. IEEE Trans. Intell. Transp. Syst. Xu Lu, Nan Zhang, Cong Tian, Bin Yu, Zhenhua Duan
2021	J	`jnl`	A Novel Load Balancing Scheme for Mobile Edge Computing. CoRR Zhenhua Duan, Cong Tian, Nan Zhang, MengChu Zhou, Bin Yu, Xiaobing Wang, Jiangen Guo, Ying Wu
2021	J	`jnl`	A dynamic approach to detecting, eliminating and fixing memory leaks. J. Comb. Optim. Bin Yu, Cong Tian, Nan Zhang, Zhenhua Duan, Hongwei Du
2021	J	`jnl`	An efficient approach for taint analysis of android applications. Comput. Secur. Jie Zhang, Cong Tian, Zhenhua Duan
2021	—	`conf`	Conditional interpolation: making concurrent program verification more effective. ESEC/SIGSOFT FSE Jie Su, Cong Tian, Zhenhua Duan
2021	C	`conf`	Design and Implementation of List and Dictionary in XD-M Language. AAIM Yajie Wang, Nan Zhang, Zhenhua Duan
2021	C	`conf`	Improving Quality of Counterexamples in Model Checking via Automated Planning. QRS Xu Lu, Cong Tian, Bin Yu, Zhenhua Duan
2021	—	`conf`	Malware Detection using CNN via Word Embedding. DSA Jie Zhang, Lin Yan, Rong Wang, Cong Tian, Zhenhua Duan
2021	J	`jnl`	Multi-matching nested relations. Theor. Comput. Sci. Jin Liu, Zhenhua Duan, Cong Tian
2021	J	`jnl`	RTPDroid: Detecting Implicitly Malicious Behaviors Under Runtime Permission Model. IEEE Trans. Reliab. Jie Zhang, Cong Tian, Zhenhua Duan, Liang Zhao
2021	—	`ed.`	Structured Object-Oriented Formal Language and Method - 10th International Workshop, SOFL+MSVL 2020, Singapore, March 1, 2021, Revised Selected Papers SOFL+MSVL Jinyun Xue, Fumiko Nagoya, Shaoying Liu, Zhenhua Duan
2021	J	`jnl`	Temporal logic specification mining of programs. Theor. Comput. Sci. Nan Zhang, Bin Yu, Cong Tian, Zhenhua Duan, Xiaoshuai Yuan
2021	J	`jnl`	Unified temporal logic. Theor. Comput. Sci. Nan Zhang, Zhenhua Duan, Cong Tian
2020	J	`jnl`	A decision procedure and complete axiomatization for projection temporal logic. Theor. Comput. Sci. Xinfeng Shu, Zhenhua Duan, Hongwei Du
2020	J	`jnl`	A novel approach to verifying context free properties of programs. Theor. Comput. Sci. Nan Zhang, Zhenhua Duan, Cong Tian, Hongwei Du
2020	A*	`conf`	Making Streett Determinization Tight. LICS Cong Tian, Wensheng Wang, Zhenhua Duan
2020	J	`jnl`	Making Streett Determinization Tight. CoRR Cong Tian, Wensheng Wang, Zhenhua Duan
2020	J	`jnl`	P2P Network Based Smart Parking System Using Edge Computing. Mob. Networks Appl. Nan Zhang, Xu Lu, Cong Tian, Zhenhua Duan, Zhifeng Sun, Ting Zhang
2020	J	`jnl`	ParRA: A Shared Memory Parallel FPGA Router Using Hybrid Partitioning Approach. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Dekui Wang, Zhenhua Duan, Cong Tian, Bohu Huang, Nan Zhang
2020	C	`conf`	Propositional Projection Temporal Logic Specification Mining. COCOA Nan Zhang, Xiaoshuai Yuan, Zhenhua Duan
2020	C	`conf`	RTPDroid: Detecting Implicitly Malicious Behaviors Under Runtime Permission Model. QRS Jie Zhang, Cong Tian, Zhenhua Duan, Liang Zhao
2020	—	`ed.`	Structured Object-Oriented Formal Language and Method - 9th International Workshop, SOFL+MSVL 2019, Shenzhen, China, November 5, 2019, Revised Selected Papers SOFL+MSVL Huaikou Miao, Cong Tian, Shaoying Liu, Zhenhua Duan
2020	C	`conf`	Transforming Multi-matching Nested Traceable Automata to Multi-matching Nested Expressions. COCOA Jin Liu, Zhenhua Duan, Cong Tian
2020	J	`jnl`	Translating Xd-C programs to MSVL programs. Theor. Comput. Sci. Meng Wang, Cong Tian, Nan Zhang, Zhenhua Duan, Chenguang Yao
2020	J	`jnl`	Verify heaps via unified model checking. Theor. Comput. Sci. Xu Lu, Zhenhua Duan, Cong Tian, Hongwei Du
2019	J	`jnl`	A temporal logic programming approach to planning. J. Comb. Optim. Kai Yang, Cong Tian, Nan Zhang, Zhenhua Duan, Hongwei Du
2019	Misc	`ed.`	Computing and Combinatorics - 25th International Conference, COCOON 2019, Xi'an, China, July 29-31, 2019, Proceedings COCOON Ding-Zhu Du, Zhenhua Duan, Cong Tian
2019	J	`jnl`	Differential Testing of Certificate Validation in SSL/TLS Implementations: An RFC-guided Approach. ACM Trans. Softw. Eng. Methodol. Cong Tian, Chu Chen, Zhenhua Duan, Liang Zhao
2019	—	`conf`	FastDroid: efficient taint analysis for Android applications. ICSE (Companion Volume) Jie Zhang, Cong Tian, Zhenhua Duan
2019	J	`jnl`	From Box Algebra to Interval Temporal Logic. Fundam. Informaticae Hanna Klaudel, Maciej Koutny, Zhenhua Duan, Ben C. Moszkowski
2019	J	`jnl`	Index set expressions can represent temporal logic formulas. Theor. Comput. Sci. Zhenhua Duan, Cong Tian, Nan Zhang, Qian Ma, Hongwei Du
2019	J	`jnl`	Model checking of pushdown systems for projection temporal logic. Theor. Comput. Sci. Liang Zhao, Xiaobing Wang, Zhenhua Duan
2019	J	`jnl`	Model checking open systems with alternating projection temporal logic. Theor. Comput. Sci. Cong Tian, Zhenhua Duan
2019	—	`ed.`	Structured Object-Oriented Formal Language and Method - 8th International Workshop, SOFL+MSVL 2018, Gold Coast, QLD, Australia, November 16, 2018, Revised Selected Papers SOFL+MSVL Zhenhua Duan, Shaoying Liu, Cong Tian, Fumiko Nagoya
2019	J	`jnl`	Verifying Full Regular Temporal Properties of Programs via Dynamic Program Execution. IEEE Trans. Reliab. Meng Wang, Cong Tian, Nan Zhang, Zhenhua Duan
2019	J	`jnl`	Verifying a scheduling protocol of safety-critical systems. J. Comb. Optim. Meng Wang, Cong Tian, Nan Zhang, Zhenhua Duan, Hongwei Du
2019	J	`jnl`	Verifying schedulability of tasks in ROS-based systems. J. Comb. Optim. Jin Cui, Cong Tian, Nan Zhang, Zhenhua Duan, Hongwei Du
2018	—	`conf`	A Blockchain Implementation of an Attendance Management System. SOFL+MSVL Jingyao Tu, Zhenhua Duan, Cong Tian, Nan Zhang, Ying Wu
2018	J	`jnl`	A Novel Approach to Modeling and Verifying Real-Time Systems for High Reliability. IEEE Trans. Reliab. Jin Cui, Zhenhua Duan, Cong Tian, Hongwei Du
2018	C	`conf`	A Novel Approach to Verifying Context Free Properties of Programs. AAIM Nan Zhang, Zhenhua Duan, Cong Tian, Hongwei Du
2018	J	`jnl`	A Runtime Optimization Approach for FPGA Routing. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Dekui Wang, Zhenhua Duan, Cong Tian, Bohu Huang, Nan Zhang
2018	J	`jnl`	A compiler for MSVL and its applications. Theor. Comput. Sci. Kai Yang, Zhenhua Duan, Cong Tian, Nan Zhang
2018	—	`conf`	Accelerating counterexample detection in software model checking. ICSE (Companion Volume) Cong Tian, Zhao Duan, Zhenhua Duan
2018	—	`conf`	Android inter-component communication analysis with intent revision. ICSE (Companion Volume) Cong Tian, Congli Xia, Zhenhua Duan
2018	—	`conf`	InterpChecker: Reducing State Space via Interpolations - (Competition Contribution). TACAS (2) Zhao Duan, Cong Tian, Zhenhua Duan, C.-H. Luke Ong
2018	J	`jnl`	On general threshold and general cascade models of social influence. J. Comb. Optim. Weili Wu, Hongwei Du, Huijuan Wang, Lidong Wu, Zhenhua Duan, Cong Tian
2018	J	`jnl`	Planning with Spatio-Temporal Search Control Knowledge. IEEE Trans. Knowl. Data Eng. Xu Lu, Cong Tian, Zhenhua Duan, Hongwei Du
2018	A*	`conf`	RFC-directed differential testing of certificate validation in SSL/TLS implementations. ICSE Chu Chen, Cong Tian, Zhenhua Duan, Liang Zhao
2018	C	`conf`	Reducing Extension Edges of Concurrent Programs for Reachability Analysis. COCOA Cong Tian, Jiaying Wang, Zhenhua Duan, Liang Zhao
2018	—	`ed.`	Structured Object-Oriented Formal Language and Method - 7th International Workshop, SOFL+MSVL 2017, Xi'an, China, November 16, 2017, Revised Selected Papers SOFL+MSVL Cong Tian, Fumiko Nagoya, Shaoying Liu, Zhenhua Duan
2018	J	`jnl`	Translating C programs to MSVL programs. CoRR Meng Wang, Cong Tian, Nan Zhang, Zhenhua Duan, Chenguang Yao
2018	J	`jnl`	Verifying temporal properties of programs: A parallel approach. J. Parallel Distributed Comput. Bin Yu, Zhenhua Duan, Cong Tian, Nan Zhang
2017	—	`conf`	Cloning Automata: Simulation and Analysis of Computer Bacteria. COCOA (1) Chu Chen, Zhenhua Duan, Cong Tian, Hongwei Du
2017	C	`ed.`	Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an, China, November 13-17, 2017, Proceedings ICFEM Zhenhua Duan, Luke Ong
2017	—	`conf`	Full regular temporal property verification as dynamic program execution. ICSE (Companion Volume) Meng Wang, Cong Tian, Zhenhua Duan
2017	—	`conf`	Implementing MapReduce with MSVL. SOFL+MSVL Nan Zhang, Meng Wang, Zhenhua Duan, Cong Tian, Jin Cui
2017	J	`jnl`	MSVL: a typed language for temporal logic programming. Frontiers Comput. Sci. Xiaobing Wang, Cong Tian, Zhenhua Duan, Liang Zhao
2017	J	`jnl`	Model Checking Multi-agent Systems with APTL. Ad Hoc Sens. Wirel. Networks Haiyang Wang, Zhenhua Duan, Cong Tian
2017	—	`conf`	Modeling and Verifying Multi-core Programs. COCOA (2) Nan Zhang, Zhenhua Duan, Cong Tian, Hongwei Du, Kai Yang
2017	A*	`conf`	More effective interpolations in software model checking. ASE Cong Tian, Zhao Duan, Zhenhua Duan, C.-H. Luke Ong
2017	—	`ed.`	Structured Object-Oriented Formal Language and Method - 6th International Workshop, SOFL+MSVL 2016, Tokyo, Japan, November 15, 2016, Revised Selected Papers SOFL+MSVL Shaoying Liu, Zhenhua Duan, Cong Tian, Fumiko Nagoya
2017	A*	`conf`	Temporalising Separation Logic for Planning with Search Control Knowledge. IJCAI Xu Lu, Cong Tian, Zhenhua Duan
2017	J	`jnl`	Two-layer hybrid peer-to-peer networks. Peer-to-Peer Netw. Appl. Zhenhua Duan, Cong Tian, MengChu Zhou, Xiaobing Wang, Nan Zhang, Hongwei Du, Lei Wang
2017	C	`conf`	Verifying Temporal Properties of C Programs via Lazy Abstraction. ICFEM Zhao Duan, Cong Tian, Zhenhua Duan
2016	A*	`conf`	A Decision Procedure for a Fragment of Linear Time Mu-Calculus. IJCAI Yao Liu, Zhenhua Duan, Cong Tian
2016	—	`conf`	A Proof System for MSVL Programs in Coq. SOFL+MSVL Lin Qian, Zhenhua Duan, Nan Zhang, Cong Tian
2016	J	`jnl`	A canonical form based decision procedure and model checking approach for propositional projection temporal logic. Theor. Comput. Sci. Zhenhua Duan, Cong Tian, Nan Zhang
2016	J	`jnl`	A complete axiom system for propositional projection temporal logic with cylinder computation model. Theor. Comput. Sci. Nan Zhang, Zhenhua Duan, Cong Tian
2016	J	`jnl`	A mechanism of function calls in MSVL. Theor. Comput. Sci. Nan Zhang, Zhenhua Duan, Cong Tian
2016	Misc	`conf`	Extending MSVL with Semaphore. COCOON Xinfeng Shu, Zhenhua Duan
2016	J	`jnl`	Linear optimal estimation for discrete-time systems with measurement-delay and packet dropping. Appl. Math. Comput. Xinmin Song, Zhenhua Duan, Ju H. Park
2016	J	`jnl`	Model checking Petri nets with MSVL. Inf. Sci. Ya Shi, Cong Tian, Zhenhua Duan, MengChu Zhou
2016	J	`jnl`	Model checking concurrent systems with MSVL. Sci. China Inf. Sci. Nan Zhang, Zhenhua Duan, Cong Tian
2016	Misc	`conf`	Satisfiability of Linear Time Mu-Calculus on Finite Traces. COCOON Yao Liu, Zhenhua Duan, Cong Tian, Bin Cui
2016	—	`ed.`	Structured Object-Oriented Formal Language and Method - 5th International Workshop, SOFL+MSVL 2015, Paris, France, November 6, 2015. Revised Selected Papers SOFL+MSVL Shaoying Liu, Zhenhua Duan
2016	J	`jnl`	Transformation from business process models to BPEL with overlapped patterns involved. Int. J. High Perform. Comput. Netw. Man Zhang, Zhenhua Duan, Qingshan Li, Hua Chu
2016	C	`conf`	Using Unified Model Checking to Verify Heaps. COCOA Xu Lu, Zhenhua Duan, Cong Tian
2016	J	`jnl`	Verifying safety critical task scheduling systems in PPTL axiom system. J. Comb. Optim. Nan Zhang, Mengfei Yang, Bin Gu, Zhenhua Duan, Cong Tian
2015	—	`conf`	A Self-ORganizing Trust Model Based on HP2P. MSN Zhenhua Duan, Yujiang Hui, Cong Tian, Nan Zhang, Bohu Huang
2015	J	`jnl`	A structural transformation from p-π to MSVL. J. Comb. Optim. Ling Luo, Zhenhua Duan, Cong Tian, Xiaobing Wang
2015	J	`jnl`	An Improved Decision Procedure for Linear Time Mu-Calculus. CoRR Yao Liu, Zhenhua Duan, Cong Tian
2015	J	`jnl`	An extended strange planet protocol. J. Comb. Optim. Jin Liu, Zhenhua Duan, Cong Tian, Nan Zhang
2015	J	`jnl`	Extending PPTL for Verifying Heap Evolution Properties. CoRR Xu Lu, Zhenhua Duan, Cong Tian
2015	J	`jnl`	Improved even order magic square construction algorithms and their applications in multi-user shared electronic accounts. Theor. Comput. Sci. Zhenhua Duan, Jin Liu, Jie Li, Cong Tian
2015	—	`conf`	LtlNfBa: Making LTL Translation More Practical. SOFL+MSVL Cong Tian, Jun Song, Zhenhua Duan, Zhao Duan
2015	Misc	`conf`	Model Checking MSVL Programs Based on Dynamic Symbolic Execution. COCOON Zhenhua Duan, Kangkang Bu, Cong Tian, Nan Zhang
2015	—	`conf`	Model Checking Process Scheduling over Multi-core Computer System with MSVL. SOFL+MSVL Xinfeng Shu, Zhenhua Duan
2015	C	`conf`	Model Checking \mu μ C/OS-III Multi-task System with TMSVL. ICFEM Jin Cui, Zhenhua Duan, Cong Tian, Nan Zhang, Conghao Zhou
2015	—	`conf`	Modeling and Verification of an Interrupt System in \mu μ C/OS-III with TMSVL. SOFL+MSVL Jin Cui, Zhenhua Duan, Cong Tian, Nan Zhang
2015	—	`conf`	PPTL_SPIN: A SPIN Based Model Checker for Propositional Projection Temporal Logic. SOFL+MSVL Xiaoming Zhang, Zhenhua Duan, Cong Tian
2015	—	`ed.`	Structured Object-Oriented Formal Language and Method - 4th International Workshop, SOFL+MSVL 2014, Luxembourg, Luxembourg, November 6, 2014, Revised Selected Papers SOFL+MSVL Shaoying Liu, Zhenhua Duan
2015	C	`conf`	Symbolic Model Checking for Alternating Projection Temporal Logic. COCOA Haiyang Wang, Zhenhua Duan, Cong Tian
2015	J	`jnl`	Transformation from PLTL to automata via NFGs. J. Comb. Optim. Cong Tian, Zhenhua Duan, Mengfei Yang
2015	C	`conf`	Verification of a real time scheduling protocol of safety-critical systems. CSCWD Meng Wang, Zhenhua Duan, Cong Tian, Nan Zhang
2015	J	`jnl`	Verification of distributed systems with the axiomatic system of MSVL. Formal Aspects Comput. Qian Ma, Zhenhua Duan, Nan Zhang, Xiaobing Wang
2014	—	`conf`	A Memory Management Mechanism for MSVL. SOFL+MSVL Kai Yang, Zhenhua Duan, Cong Tian
2014	J	`jnl`	A formal proof of the deadline driven scheduler in PPTL axiomatic system. Theor. Comput. Sci. Nan Zhang, Zhenhua Duan, Cong Tian, Ding-Zhu Du
2014	J	`jnl`	A practical decision procedure for Propositional Projection Temporal Logic with infinite models. Theor. Comput. Sci. Zhenhua Duan, Cong Tian
2014	Misc	`conf`	An Axiomatization for Cylinder Computation Model. COCOON Nan Zhang, Zhenhua Duan, Cong Tian
2014	Misc	`conf`	An Improved Recursive Algorithm for Parity Games. TASE Yao Liu, Zhenhua Duan, Cong Tian
2014	J	`jnl`	Buchi Determinization Made Tighter. CoRR Cong Tian, Zhenhua Duan
2014	—	`conf`	Clustering and Partition Based Divide and Conquer for SAT Solving. MSN Quanrun Fan, Zhenhua Duan, Cong Tian, Hongwei Du
2014	C	`conf`	Extending MSVL with Function Calls. ICFEM Nan Zhang, Zhenhua Duan, Cong Tian
2014	C	`conf`	Improved Even Order Magic Square Construction Algorithms and Their Applications. COCOA Zhenhua Duan, Jin Liu, Jie Li, Cong Tian
2014	C	`conf`	Interval Temporal Logic Semantics of Box Algebra. LATA Hanna Klaudel, Maciej Koutny, Zhenhua Duan
2014	J	`jnl`	Linear time-dependent constraints programming with MSVL. J. Comb. Optim. Qian Ma, Zhenhua Duan
2014	J	`jnl`	Making CEGAR More Efficient in Software Model Checking. IEEE Trans. Software Eng. Cong Tian, Zhenhua Duan, Zhao Duan
2014	B	`conf`	Model Checking Rate-Monotonic Scheduler with TMSVL. ICECCS Jin Cui, Zhenhua Duan, Cong Tian
2014	Misc	`conf`	Normal Form Expressions of Propositional Projection Temporal Logic. COCOON Zhenhua Duan, Cong Tian, Nan Zhang
2014	J	`jnl`	Secure communications with strange planet protocol. Optim. Lett. Cong Tian, Zhenhua Duan, Jin Liu
2014	C	`conf`	Simulation and verification of the virtual memory management system with MSVL. CSCWD Meng Wang, Zhenhua Duan, Cong Tian
2014	—	`ed.`	Structured Object-Oriented Formal Language and Method - Third International Workshop, SOFL+MSVL 2013, Queenstown, New Zealand, October 29, 2013, Revised Selected Papers SOFL+MSVL Shaoying Liu, Zhenhua Duan
2014	—	`conf`	Unified Bounded Model Checking for MSVL. SOFL+MSVL Bin Yu, Zhenhua Duan, Cong Tian
2013	C	`conf`	A Transformation from p-π to MSVL. ICTAC Ling Luo, Zhenhua Duan
2013	J	`jnl`	A complete proof system for propositional projection temporal logic. Theor. Comput. Sci. Zhenhua Duan, Nan Zhang, Maciej Koutny
2013	J	`jnl`	A cylinder computation model for many-core parallel computing. Theor. Comput. Sci. Nan Zhang, Zhenhua Duan, Cong Tian
2013	C	`conf`	An Extended Strange Planet Protocol. COCOA Jin Liu, Zhenhua Duan, Cong Tian
2013	Misc	`conf`	Bounded Model Checking for Propositional Projection Temporal Logic. COCOON Zhenhua Duan, Cong Tian, Mengfei Yang, Jia He
2013	—	`conf`	Bounded Model Checking of Traffic Light Control System. TTSS Bin Yu, Zhenhua Duan, Cong Tian
2013	A*	`conf`	Detecting spurious counterexamples efficiently in abstract model checking. ICSE Cong Tian, Zhenhua Duan
2013	Misc	`conf`	Deternimization of Büchi Automata as Partitioned Automata. COCOON Cong Tian, Zhenhua Duan, Mengfei Yang
2013	—	`conf`	Formalizing and Implementing Types in MSVL. SOFL+MSVL Xiaobing Wang, Zhenhua Duan, Liang Zhao
2013	J	`jnl`	ITL semantics of composite Petri nets. J. Log. Algebraic Methods Program. Zhenhua Duan, Hanna Klaudel, Maciej Koutny
2013	—	`conf`	Improved Net Reductions for LTL $$\setminus $$ \ X Model Checking. SOFL+MSVL Ya Shi, Zhenhua Duan, Cong Tian, Hua Yang
2013	—	`conf`	Integrating Separation Logic with PPTL. SOFL+MSVL Xu Lu, Zhenhua Duan, Cong Tian, Hongjin Liu
2013	Misc	`conf`	Integration of Linear Constraints with a Temporal Logic Programming Language. TASE Qian Ma, Zhenhua Duan, Mengfei Yang
2013	—	`conf`	Modeling and Verification of RBC Handover Protocol. TTSS Kai Yang, Zhenhua Duan, Cong Tian
2013	—	`conf`	Present-Future Form of Linear Time $$\mu $$ -Calculus. SOFL+MSVL Yao Liu, Zhenhua Duan, Cong Tian, Bo Liu
2013	C	`conf`	Simulation of CTCS-3 protocol with temporal logic programming. CSCWD Peng Zhang, Zhenhua Duan, Cong Tian
2013	—	`conf`	Some Fixed-Point Issues in PPTL. Theories of Programming and Formal Methods Zhenhua Duan, Qian Ma, Cong Tian, Nan Zhang
2013	C	`conf`	Translation from Workflow Nets to MSVL. ICFEM Ya Shi, Zhenhua Duan, Cong Tian
2012	—	`conf`	Abstract Model Checking with SOFL Hierarchy. SOFL Cong Tian, Shaoying Liu, Zhenhua Duan
2012	J	`jnl`	An efficient approach for abstraction-refinement in model checking. Theor. Comput. Sci. Cong Tian, Zhenhua Duan, Nan Zhang
2012	J	`jnl`	Efficient and scalable scheduling for performance heterogeneous multicore systems. J. Parallel Distributed Comput. Pengcheng Nie, Zhenhua Duan
2012	—	`conf`	Model Checking C Programs with MSVL. SOFL Yan Yu, Zhenhua Duan, Cong Tian, Mengfei Yang
2012	—	`ch.`	Model Checking. Handbook of Finite State Based Models and Applications Zhenhua Duan, Cong Tian
2012	Misc	`conf`	Symbolic Model Checking for Propositional Projection Temporal Logic. TASE Tao Pang, Zhenhua Duan, Cong Tian
2012	C	`conf`	Time Constraints with Temporal Logic Programming. ICFEM Meng Han, Zhenhua Duan, Xiaobing Wang
2011	Misc	`ed.`	5th IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2011, Xi'an, China, 29-31 August 2011 TASE Zhenhua Duan, C.-H. Luke Ong
2011	C	`conf`	A Semantic Model for Many-Core Parallel Computing. COCOA Nan Zhang, Zhenhua Duan
2011	C	`conf`	Asynchronous Communication in MSVL. ICFEM Dapeng Mo, Xiaobing Wang, Zhenhua Duan
2011	J	`jnl`	Detecting Spurious Counterexamples Efficiently in Abstract Model Checking CoRR Cong Tian, Zhenhua Duan
2011	C	`conf`	ESHMP: A Stall-Time-Based Scheduling for Performance Heterogeneous Multicore Systems. HPCC Pengcheng Nie, Zhenhua Duan, Bohu Huang
2011	J	`jnl`	Expressiveness of propositional projection temporal logic with star. Theor. Comput. Sci. Cong Tian, Zhenhua Duan
2011	Misc	`conf`	Focus Game for Projection Temporal Logic. TASE Cong Tian, Zhenhua Duan
2011	Misc	`conf`	Making Abstraction-Refinement Efficient in Model Checking. COCOON Cong Tian, Zhenhua Duan
2011	C	`conf`	Public Communication Based on Russian Cards Protocol: A Case Study. COCOA Jia He, Zhenhua Duan
2011	—	`conf`	Specification and Verification of UML2.0 Sequence Diagrams Using Event Deterministic Finite Automata. SSIRI (Companion) Chen Zhang, Zhenhua Duan
2010	—	`conf`	A Transformation from PPTL to S1S. COCOA (2) Cong Tian, Zhenhua Duan
2010	C	`conf`	Alternating Interval Based Temporal Logics. ICFEM Cong Tian, Zhenhua Duan
2010	—	`conf`	An Executable Concurrent Model for OWL-S Process Models. QSIC Zhenhua Duan, Cong Tian
2010	C	`conf`	An Improved Decision Procedure for Propositional Projection Temporal Logic. ICFEM Zhenhua Duan, Cong Tian
2010	Misc	`conf`	Axiomatic Temporal Logic Programs Verification. TASE Xiaoxiao Yang, Zhenhua Duan
2010	J	`jnl`	Axiomatic semantics of projection temporal logic programs. Math. Struct. Comput. Sci. Xiaoxiao Yang, Zhenhua Duan, Qian Ma
2010	J	`jnl`	Making Abstraction Refinement Efficient in Model Checking CoRR Cong Tian, Zhenhua Duan
2010	Misc	`conf`	Model Checking Rectangular Hybrid Systems with Timed Computation Tree Logic. TASE Haibin Zhang, Zhenhua Duan, Bohu Huang, Xiaobing Wang, Long Zhang
2010	—	`conf`	Non-Functional Requirements Elicitation and Incorporation into Class Diagrams. IIP Xiaoyu Song, Zhenhua Duan, Cong Tian
2010	J	`jnl`	Unconditional secure communication: a Russian Cards protocol. J. Comb. Optim. Zhenhua Duan, Chen Yang
2009	—	`conf`	A Model-Driven Approach for Generating Business Processes and Process Interaction Semantics. ACIS-ICIS Chenting Zhao, Zhenhua Duan, Man Zhang
2009	—	`ch.`	A Proof System for Projection Temporal Logic. Computer and Information Science Zhenhua Duan, Xinfeng Shu
2009	J	`jnl`	A note on stutter-invariant PLTL. Inf. Process. Lett. Cong Tian, Zhenhua Duan
2009	Misc	`conf`	An Efficient Algorithm for Finding Empty Space for Reconfigurable Systems. TASE Yan Xiao, Zhenhua Duan, Pengcheng Nie
2009	J	`jnl`	Complexity of propositional projection temporal logic with star. Math. Struct. Comput. Sci. Cong Tian, Zhenhua Duan
2009	C	`conf`	Generalized Russian Cards Problem. COCOA Zhenhua Duan, Chen Yang
2009	—	`conf`	Verification of Use Case with Petri Nets in Requirement Analysis. ICCSA (2) Jinqiang Zhao, Zhenhua Duan
2008	—	`ed.`	8th International Conference on Application of Concurrency to System Design (ACSD 2008), Xi'an, China, June 23-27, 2008 ACSD Jonathan Billington, Zhenhua Duan, Maciej Koutny
2008	Misc	`conf`	A Complete Axiomatization of Propositional Projection Temporal Logic. TASE Zhenhua Duan, Nan Zhang
2008	C	`conf`	A Unified Model Checking Approach with Projection Temporal Logic. ICFEM Zhenhua Duan, Cong Tian
2008	J	`jnl`	A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica Zhenhua Duan, Cong Tian, Li Zhang
2008	—	`conf`	Dynamic Critical-Path based on Fit Degree scheduling for reconfigurable multi-FPGAs. ACSD Yan Xiao, Zhenhua Duan
2008	J	`jnl`	Framed temporal logic programming. Sci. Comput. Program. Zhenhua Duan, Xiaoxiao Yang, Maciej Koutny
2008	A	`conf`	From Business Process Models to Web Services Orchestration: The Case of UML 2.0 Activity Diagram to BPEL. ICSOC Man Zhang, Zhenhua Duan
2008	C	`conf`	Kapa: A File Sharing System Based on HP2P. ICIW Bo Wang, Zhenhua Duan, Lei Wang
2008	J	`jnl`	Operational semantics of Framed Tempura. J. Log. Algebraic Methods Program. Xiaoxiao Yang, Zhenhua Duan
2008	C	`conf`	Propositional Projection Temporal Logic, Bchi Automata and omega-Regular Expressions. TAMC Cong Tian, Zhenhua Duan
2008	C	`conf`	Semi-automatically annotating data semantics to web services using ontology mapping. CSCWD Man Zhang, Zhenhua Duan, Chenting Zhao
2008	C	`conf`	Symbolic Algorithm Analysis of Rectangular Hybrid Systems. TAMC Haibin Zhang, Zhenhua Duan
2008	C	`ed.`	Theory and Applications of Models of Computation, 5th International Conference, TAMC 2008, Xi'an, China, April 25-29, 2008. Proceedings TAMC Manindra Agrawal, Ding-Zhu Du, Zhenhua Duan, Angsheng Li
2007	Misc	`conf`	An Interpreter for Framed Tempura and Its Application. TASE Yongtao Ma, Zhenhua Duan, Xiaobing Wang, Xiaoxiao Yang
2007	C	`conf`	Automating Web Service Composition for Collaborative Business Processes. CSCWD Lihui Lei, Zhenhua Duan
2007	C	`conf`	Decidability of Propositional Projection Temporal Logic with Infinite Models. TAMC Zhenhua Duan, Cong Tian
2007	C	`conf`	HP2P: A Hybrid Hierarchical P2P Network. ICDS Zhuo Peng, Zhenhua Duan, Jian-Jun Qi, Yang Cao, Ertao Lv
2007	C	`conf`	Incorporating Clusters into Hybrid P2P Network. ICDS Ertao Lv, Zhenhua Duan, Jian-Jun Qi, Yang Cao, Zhuo Peng
2007	J	`jnl`	Integrating AJAX and Web Services for Cooperative Image Editing. IT Prof. Lihui Lei, Zhenhua Duan
2007	C	`conf`	Model Checking Propositional Projection Temporal Logic Based on SPIN. ICFEM Cong Tian, Zhenhua Duan
2007	—	`conf`	Operational Semantics of Framed Temporal Logic Programs. SOFSEM (1) Xiaoxiao Yang, Zhenhua Duan
2007	—	`conf`	Utilizing Fuzzy Petri Net for Choreography Based Semantic Web Services Discovery. ICATPN Peng Men, Zhenhua Duan, Bin Yu
2006	—	`conf`	A Comprehensive Framework for Dynamic Web Services Integration. ECOWS Zhile Zou, Zhenhua Duan, Jianli Wang
2006	—	`conf`	Building Business Processes or Assembling Service Components: Reuse Services with BPEL4WS and SCA. ECOWS Zhile Zou, Zhenhua Duan
2006	—	`conf`	Implementing Chord for HP2P Network. OTM Workshops (2) Yang Cao, Zhenhua Duan, Jian-Jun Qi, Zhuo Peng, Ertao Lv
2006	C	`conf`	Semantic Matching of Web Services Based on Choreographies. CSCWD Lihui Lei, Zhenhua Duan, Bin Yu
2006	—	`conf`	Semantic Matching of Web Services for Collaborative Business Processes. CSCWD (Selected Papers) Lihui Lei, Zhenhua Duan, Bin Yu
2006	A	`conf`	Transforming OWL-S Process Model into EDFA for Service Discovery. ICWS Lihui Lei, Zhenhua Duan
2005	B	`conf`	Semantics of Framed Temporal Logic Programs. ICLP Zhenhua Duan, Xiaoxiao Yang, Maciej Koutny
2004	J	`jnl`	A Framed Temporal Logic Programming Language. J. Comput. Sci. Technol. Zhenhua Duan, Maciej Koutny
1996	—	`—`	An extended interval temporal logic and a framing technique for temporal logic programming. Zhenhua Duan
1994	B	`conf`	Projection in Temporal Logic Programming. LPAR Zhenhua Duan, Maciej Koutny, Chris Holt