Back to Home

2016

 

Journal papers:

 

• Ya shi, Cong Tian*, Zhenhua Duan*. Model Checking Petri Nets with MSVL. Information Sciences, Vol 363: 274-291. DOI: 10.1016/j.ins.2016.01.036

 

• Zhenhua Duan, Cong Tian*, Mengchu Zhou, Xiaobing Wang, Nan Zhang, Hongwei Du, Lei Wang. Two-la[ant]yer hybrid peer-to-peer networks. Peer-to-Peer Networking and Applications. DOI: 10.1007/s12083-016-0460-5.

 

• Nan Zhang, Zhenhua Duan*, Cong Tian*. A Mechanism of Function Calls in MSVL，Theoretical Computer Science, doi:10.1016/j.tcs.2016.02.037.

 

 Conference papers:

 

• Yao Liu, Zhenhua Duan*, Cong Tian*. A Decision Procedure for A Fragment of Linear-Time Mu-Calculus. Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI 2016)，1195 - 1201.

 

2015

Journal papers:

 

• Zhenhua Duan, Cong Tian*, and Nan Zhang. A Canonical Form Based Decision Procedure and Model Checking Approach for Propositional Projection Temporal Logic. Theoretical Computer Science, 609: 544-560, 2016.  doi:10.1016/j.tcs.2015.08.039. 

 

• Zhenhua Duan, Jin Liu, Jie Li, Cong Tian*. Improved Even Order Magic Square Construction Algorithms and Their Applications in Multi-user Shared Electronic Accounts. Theoretical Computer Science, 607: 391-410. 10.1016/j.tcs.2015.07.053. 

 

• Nan Zhang, Zhenhua Duan, and Cong Tian. A Complete Axiomation for Propositional Projection Temporal Logic with cylinder computation model. Theorectical Computer Science. DOI:10.1016/J.TCS.2015.05.007,2015. 

 

• Jin Liu, Zhenhua Duan, Cong Tian, and Nan Zhang. An extended strange planet protocol. Journal of Combinatorial Optimization, Volume 30, Issue 2, pp 299-319, Aug 2015.

 

• Ling Luo, Zhenhua Duan, Cong Tian, and Xiaobing Wang. A structural transformation from p-π to MSVL. Journal of Combinatorial Optimization, Volume 29, Issue 1 pp 308-329, Jan 2015.

 

• Cong Tian and Zhenhua Duan. Transformation from PLTL to Automata via NFGs. Journal of Combinatorial Optimization, 29 (2), 406-417, 2015. 

 

Conference papers:

• Jin Cui, Zhenhua Duan, Cong Tian, and Nan Zhang. Model Checking of a muC/OS-III Multi-task System with TMSVL. The 17th International Conference on Formal Engineering Methods (ICFEM 2015), Springer-Verlag, LNCS 9407, 187-200, 2015.

 

• Zhenhua Duan, Kangkang Bu, Cong Tian, Nan Zhang. Model Checking MSVL Programs Based on Dynamic Symbolic Execution. In proceedings of the 21th Annual International Computing and Combinatorics Conference (COCOON 2015), Springer-Verlag, LNCS 9198, pp 521-533, 2015.  

 

2014

Journal papers:

• Kai Yang, Zhenhua Duan, and Cong Tian. Modeling and Verification of RBC Handover Protocol. Electronic Notes in Theoretical Computer Science,Volume 309, Pages 51–62, 22 December 2014.

 

• Bin Yu, Zhenhua Duan, and Cong Tian. Bounded Model Checking of Traffic Light Control System. Electronic Notes in Theoretical Computer Science,Volume 309, Pages 63–74, 22 December 2014.

 

• Cong Tian, Zhenhua Duan, and Zhao Duan. Making CEGAR More Efficient in Software Model Checking. IEEE Transactions on Software Engineering (TSE), Vol 40(12), 1206-1223, Dec 2014. DOI:10.1109/TSE.2014.2357442, 2014.

 

• Zhenhua Duan and Cong Tian. A Practical Decision Procedure for Propositional Projection Temporal Logic with Infinite Models. Theorectical Computer Science. Vol 554,  pp. 169-190, 2014. Doi:10.1016/j.tcs.2014.02.011

 

• Nan Zhang, Zhenhua Duan, Cong Tian, and Dingzhu Du. A formal proof of the deadline driven scheduler in PPTL axiomatic system.Theoretical Computer Science. Vol 554,  pp. 229-253, 2014. Doi:10.1016/j.tcs.2013.12.014

 

• Cong Tian, Shaoying Liu, and Zhenhua Duan. Test Case Generation from Conjunctions of Predicates with Model Checking. Chinese Journal of Electronics, Vol 23, No 2, 271-277, 2014.

 

• Cong Tian, Zhenhua Duan, and Jin Liu. Secure Communications with Strange Planet Protocol.  Optimization Letters, 8(1), 201-209, 2014. DOI:10.1007/s11590-012-0561-x.

 

Conference papers:

• Zhenhua Duan and Cong Tian. Normal Form ex[ant]pressions for Propositional Projection Temporal Logic. In proceedings of the 20th Annual International Computing and Combinatorics Conference (COCOON 2014), LNCS 8591, pp 84-93, Atlanta, Georgia, USA, 2014.

 

• Nan Zhang, Zhenhua Duan and Cong Tian. An Axiomatization for Cylinder Computation Model. In proceedings of the 20th Annual International Computing and Combinatorics Conference (COCOON 2014), LNCS 8591, pp 71-83, Atlanta, Georgia, USA, 2014.

 

• Bo Zhou, Xin Xia, David Lo, Cong Tian, and Xinyu Wang. Towards More Accurate Content Categorization of API Discussions. In proceedings of the 22th International Conference on Program Comprehension (ICPC 2014), PP. 95-105, Hyderabad, India, 2014.

 

• Yao Liu, Zhenhua Duan, and Cong Tian. An Improved Recursive Algorithm for Parity Games. The 8th International Symposium on Theoretical Aspects of Software Engineering(TASE 2014), pp 154-161, 2014.

 

• Jin Cui, Zhenhua Duan, and Cong Tian. Model Checking Rate-Monotonic Scheduler with TMSVL. The 19th International Conference on Engineering of Complex ComputerSystems(ICECCS 2014), pp 202-205, 2014.

 

• Kai Yang, Zhenhua Duan, Cong Tian. A Memory Management Mechanism for MSVL. SOFL+MSVL 2014: 179-188

 

• Bin Yu, Zhenhua Duan, Cong Tian. Unified Bounded Model Checking for MSVL. SOFL+MSVL 2014: 49-61

 

• Quanrun Fan, Zhenhua Duan, Cong Tian, Hongwei Du. Clustering and Partition Based Divide and Conquer for SAT Solving. MSN 2014: 299-307

 

• Nan Zhang, Zhenhua Duan, Cong Tian. Extending MSVL with Function Calls. the 17th International Conference on Formal Engineering Methods (ICFEM 2015),446-458.

 

• Meng Wang, Zhenhua Duan, Cong Tian.Simulation and verification of the virtual memory management system with MSVL. CSCWD 2014: 360-365

 

• Zhenhua Duan, Jin Liu, Jie Li, Cong Tian. Improved Even Order Magic Square Construction Algorithms and Their Applications. COCOA 2014: 666-680

 

2013

Journal papers:

• Nan Zhang, Zhenhua Duan, and Cong Tian. Verifying a Carry Look-Ahead Adder with Propositional Projection Temporal Logic. Chinese Journal of Electronics, Vol 22, Issue (CJE-1): 21-24, 2013.

 

Conference papers:

• Jin Liu, Zhenhua Duan, and Cong Tian. An Extended Strange Planet Protocol. In proceedings of the 7th Annual International Conference on Combinatorial Optimization and Applications (COCOA 2013), LNCS 8287, Springer-Verlag, pp 214-225.

 

• Ya Shi, Zhenhua Duan, and Cong Tian. Translation from Workflow Nets to MSVL.  In Proceedings of the 15th International Conference on Formal Engineering Methods (ICFEM 2013), LNCS 8144, Springer-Verlag, pp 281-296, 2013.

 

• Xu Lu, Zhenhua Duan, Cong Tian, and Hongjin Liu. Integrating Separation Logic with PPTL. SOFL+MSVL 2013, 35-47.

 

• Ya Shi, Zhenhua Duan, Cong Tian, and Hua Yang. Improving Net Reductions for LTLX Model Checking. SOFL+MSVL 2013, 48-61.

 

• Yao Liu, Zhenhua Duan, Cong Tian, and Bo Liu.  Present-Future Form of Linear Time Mu-Calculus. SOFL+MSVL 2013, 76-85.

 

• Peng Zhang, Zhenhua Duan, and Cong Tian. Simulation of CTCS-3 Protocol with Temporal Logic Programming. CSCWD 2013, 72-77.

 

• Zhenhua Duan, Qian Ma, Cong Tian, and Nan Zhang. Some Fixed-Point Issues in PPTL. Theories of Programming and Formal Methods 2013,151-165,2013.

 

• Cong Tian, Zhenhua Duan and Mengfei Yang. Deternimization of Büchi Automata as Partitioned Automata. Proceedings of the 19th Annual International Computing and Combinatorics Conference (COCOON 2013), 158-168, 2013.

 

• Zhenhua Duan, Cong Tian, Mengfei Yang and Jia He. Bounded Model Checking for Propositional Projection Temporal Logic.  Proceedings of the 19th Annual International Computing and Combinatorics Conference (COCOON 2013), 591-602, 2013.

 

• Cong Tian and Zhenhua Duan. Detecting Spurious Counterexamples Efficiently in Abstract Model Checking.  Proceedings of the 35th International Conference on Software Engineering (ICSE 2013), 202-211, 2013.

 

• Cong Tian, Shaoying Liu and Zhenhua Duan. Abstract Model Checking with SOFL Hierachy.  Proceedings of  WSOFL 2012, LNCS 7787, 71-86, 2013.

 

• Yan Yu, Zhenhua Duan, Cong Tian and Mengfei Yang. Model Checking C Programs with MSVL.  Proceedings of  WSOFL 2012, LNCS 7787, 87-103, 2013.

 

Papers in Chinese:

 

• Pengcheng Nie, Zhenhua Duan, Cong Tian, and Mengfei Yang. Adaptive Scheduling on Performance Asymmetric Multicore Processors,Chinese Journal of Computers,2013, 36(4),773-781.

 

2012

Journal papers:

• Cong Tian, Zhenhua Duan. An Efficient Approach for Abstraction Refinement in Model Checking. Theoretical Computer Science, Vol 461, 76-85, 2012. DOI:10.1016/j.tcs.2011.12.014

 

• Nan Zhang, Zhenhua Duan, and Cong Tian. A cylinder computation model for many-core parallel computing. Theoretical Computer Science(2012), Vol: 497, 68-83, 2013, doi:10.1016/j.tcs.2012.02.011.

 

Conference papers:

• Cong Tian and Zhenhua Duan. A Practical Transformation from LTL to Automata. CNSI 2012, pp.638-643, 2012.

 

• Tao Pang, Zhenhua Duan, Cong Tian. Symbolic Model Checking for Propositional Projection Temporal Logic. TASE 2012: 9-16.

 

Chapters:

• Zhenhua Duan and Cong Tian. Temporal Logic and Model Checking. Handbook of Finite State Based Models and Applications. SBN-10:1439846189. Chapman & Hall. Aug 2012.

 

2011

Journal papers:

• Cong Tian and Zhenhua Duan, Expressiveness of  Propositional Projection Temporal Logic, Theoretical Computer Science, Volume 412, Issue 18, Aug, 2011, Pages 1729-1744. DOI:10.1016/j.tcs.2010.12.047.

 

Conference papers:

• Sven Schewe and Cong Tian. Synthesising Classic and Interval Temporal Logic. In the proceedings of the 18th International Symposium on Temporal Representation and Reasoning (TIME 2011), 64-71, IEEE Computer Society, 2011.  

 

• Cong Tian and Zhenhua Duan. Focus Game for PITL with Infinite Models. In the proceedings of TASE 2011, 45-51, IEEE Computer Society, 2011.

 

• Cong Tian and Zhenhua Duan. Making Abstraction Refinement Efficient in Model Checking. The 17th International Conference COCOON 2011,Springer-verlag LNCS 6842, 90-111, 2011.

 

• Cong Tian, Shaoying Liu and Shin Nakajima. Utilizing Model Checking for Automatic Test Case Generation from Conjunctions of Predicates. The proceedings of CSTAV 2011, 304-309, IEEE Conputer Society.

 

Papers in Chinese:

• Cong Tian, Zhenhua Duan. Model Checking Rate Monotonic Scheduling Algorithm based on Propositional Projection Temporal Logic. Journal of Software,2011,22(2):211-221.

 

• Chen Zhang, Zhenhua Duan, Cong Tian. Specification and Verification of UML2.0 Sequence Diagrams based on Event Deterministic Finite Automata. Journal of Software,2011,22(11):2625-2638.

 

2010

Conference papers:

• Cong Tian and Zhenhua Duan. A Transformation from PPTL to S1S. In the proceedings of COCOA 2010. Part 2, LNCS 6509, 374-386, 2010.

 

• Cong Tian and Zhenhua Duan. Alternating Interval based Temporal Logics. Proceedings of 12th International Conference on Formal EngineeringMethods (ICFEM2010), LNSC 6447, Springer-Verlag,16-19 Nov. 2010, pp. 694-709.

 

• Zhenhua Duan and Cong Tian. An Improved Decision Procedure for Propositional Projection Temporal Logic. Proceedings of 12th International Conference on Formal EngineeringMethods (ICFEM2010), LNSC 6447, Springer-Verlag,16-19 Nov. 2010, pp. 90-105.

 

• Xiaoyu Song, Zhenhua Duan, and Cong Tian. Non-Functional Requirements Elicitation and Incorporation into Class Diagrams. Intelligent Information Processing 2010: 72-81.

 

• Zhenhua Duan and Cong Tian. An Executable Concurrent Model for OWL-S Process Models. QSIC 2010, pp. 405-413, IEEE Conputer Society, July 2010.

 

2009

Journal papers:

• Cong Tian and Zhenhua Duan, A Note on Stutter-Invariant  PLTL, Information Processing Letters, 109 (13): 663-667, 2009.

 

• Cong Tian and  Zhenhua Duan,  Complexity of Propositional Projection Temporal Logic with Star,  Mathematical Structures in Computer Science, vol.19, pp.73-100, Cambridge University Press, 2009.

 

2008

Journal papers:

• Zhenhua Duan, Cong Tian, and Li Zhang, A Decision Procedure for Propositional Projection Temporal Logic with Infinite Models. Acta Informatica, 45(1),43-78, Springer-verlag, 2008.

 

Conference papers:

• Zhenhua Duan and Cong Tian, A Unified Model checking Approach with Projection Temporal Logic, ICFEM2008,LNCS5256, pp 167-186, Springer-verlag, Oct, 2008.

 

• Cong Tian and Zhenhua Duan, Propositional Projection Temporal Logic, Buchi Automata and omega-Regular ex[ant]pressions, TAMC 2008,  LNCS 4978, pp 47-58, Springer-verlag, April, 2008.

 

2007

Conference papers:

• Cong Tian and Zhenhua Duan, Model Checking Propositional Projection Temporal Logic based on SPIN. ICFEM 2007, LNCS4789 , pp 246-265, Springer-verlag, Nov, 2007.

 

• Zhenhua Duan and Cong Tian, Decidability of Propositional Projection Temporal Logic with Infinite Models. TAMC 2007, LNCS4484 , pp 521-532, Springer-verlag, May, 2007.