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, andCong 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 Tianand 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, andCong 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, andCong 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 andCong 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 andCong 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 andCong 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 22thInternational Conference on Program Comprehension (ICPC 2014), PP. 95-105,Hyderabad, India, 2014.

• Yao Liu, Zhenhua Duan, andCong 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, andCong 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, andCong 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, andCong 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, andCong 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, andCong 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 Tianand 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 Tianand 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, andCong 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 Tianand 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 andCong 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 Tianand 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 andCong Tian.Synthesising Classic and Interval Temporal Logic. In the proceedings of the 18th International Symposium on Temporal Representation and Reasoning (TIME2011), 64-71, IEEE Computer Society, 2011.

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

• Cong Tianand 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 TianandZhenhua Duan.A Transformation from PPTL to S1S. In the proceedings of COCOA 2010. Part 2, LNCS 6509, 374-386, 2010.

• Cong Tianand 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 andCong 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, andCong Tian.Non-Functional Requirements Elicitation and Incorporation into Class Diagrams. Intelligent Information Processing 2010: 72-81.

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

2009

Journal papers:

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

• Cong Tianand 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 andCong Tian,A Unified Model checking Approach with Projection Temporal Logic, ICFEM2008,LNCS5256, pp 167-186, Springer-verlag, Oct, 2008.

• Cong Tianand 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 Tianand Zhenhua Duan,Model Checking Propositional Projection Temporal Logic based on SPIN. ICFEM 2007, LNCS4789 , pp 246-265, Springer-verlag, Nov, 2007.

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