1. Model checking Petri nets with MSVL. Ya Shi, Cong Tian, Zhenhua Duan, Mengchu Zhou: Inf. Sci. 363: 274-291 (2016)
  2. Extending MSVL with Semaphore. Xinfeng Shu, Zhenhua Duan: COCOON 2016: 599-610
  3. Verification of distributed systems with the axiomatic system of MSVL. Qian Ma, Zhenhua Duan, Nan Zhang, Xiaobing Wang: Formal Asp. Comput. 27(1): 103-131 (2015)
  4. A structural transformation from p-π to MSVL. Ling Luo, Zhenhua Duan, Cong Tian, Xiaobing Wang: J. Comb. Optim. 29(1): 308-329 (2015)
  5. Model Checking MSVL Programs Based on Dynamic Symbolic Execution. Zhenhua Duan, Kangkang Bu, Cong Tian, Nan Zhang: COCOON 2015: 521-533
  6. Model Checking μμC OS-III Multi-task System with TMSVL. Jin Cui, Zhenhua Duan, Cong Tian, Nan Zhang, Conghao Zhou: ICFEM 2015: 187-200
  7. Modeling and Verification of an Interrupt System in μμC OS-III with TMSVL.Jin Cui, Zhenhua Duan, Cong Tian, Nan Zhang: SOFL+MSVL 2015: 15-28
  8. Model Checking Process Scheduling over Multi-core Computer System with MSVL. Xinfeng Shu, Zhenhua Duan: SOFL+MSVL 2015: 103-117
  9. Linear time-dependent constraints programming with MSVL. Qian Ma, Zhenhua Duan: J. Comb. Optim. 27(4): 724-766 (2014)
  10. Making CEGAR More Efficient in Software Model Checking. Cong Tian, Zhenhua Duan, Zhao Duan: IEEE Trans. Software Eng. 40(12): 1206-1223 (2014)
  11. An Axiomatization for Cylinder Computation Model. Nan Zhang, Zhenhua Duan, Cong Tian: COCOON 2014: 71-83
  12. Simulation and verification of the virtual memory management system with MSVL.Meng Wang, Zhenhua Duan, Cong Tian: CSCWD 2014: 360-365
  13. Model Checking Rate-Monotonic Scheduler with TMSVL. Jin Cui, Zhenhua Duan, Cong Tian: ICECCS 2014: 202-205
  14. Extending MSVL with Function Calls. Nan Zhang, Zhenhua Duan, Cong Tian: ICFEM 2014: 446-458
  15. Unified Bounded Model Checking for MSVL.Bin Yu, Zhenhua Duan, Cong Tian: SOFL+MSVL 2014: 49-61
  16. A Memory Management Mechanism for MSVL.Kai Yang, Zhenhua Duan, Cong Tian: SOFL+MSVL 2014: 179-188
  17. Simulation of CTCS-3 protocol with temporal logic programming. Peng Zhang, Zhenhua Duan, Cong Tian: CSCWD 2013: 72-77
  18. Translation from Workflow Nets to MSVL. Ya Shi, Zhenhua Duan, Cong Tian: ICFEM 2013: 281-296
  19. Formalizing and Implementing Types in MSVL.Xiaobing Wang, Zhenhua Duan, Liang Zhao: SOFL+MSVL 2013: 62-75
  20. Integration of Linear Constraints with a Temporal Logic Programming Language.Qian Ma, Zhenhua Duan, Mengfei Yang: TASE 2013: 157-164
  21. Efficient and scalable scheduling for performance heterogeneous multicore systems. Pengcheng Nie, Zhenhua Duan: J. Parallel Distrib. Comput. 72(3): 353-361
  22. An efficient approach for abstraction-refinement in model checking. Cong Tian, Zhenhua Duan, Nan Zhang: Theor. Comput. Sci. 461: 76-85 (2012)
  23. Model Checking C Programs with MSVL.Yan Yu, Zhenhua Duan, Cong Tian, Mengfei Yang: SOFL 2012: 87-103
  24. Asynchronous Communication in MSVL.Dapeng Mo, Xiaobing Wang, Zhenhua Duan: ICFEM 2011: 82-97
  25. Operational semantics of Framed Tempura. Xiaoxiao Yang, Zhenhua Duan: J. Log. Algebr. Program. 78(1): 22-51 (2008)
  26. Framed temporal logic programming. Zhenhua Duan, Xiaoxiao Yang, Maciej Koutny: Sci. Comput. Program. 70(1): 31-61 (2008)