A decision procedure for propositional projection temporal logic with infinite models Z Duan, C Tian, L Zhang Acta Informatica 45 (1), 43-78, 2008 | 164 | 2008 |

A unified model checking approach with projection temporal logic Z Duan, C Tian International Conference on Formal Engineering Methods, 167-186, 2008 | 81 | 2008 |

Complexity of propositional projection temporal logic with star C Tian, Z Duan Mathematical Structures in Computer Science 19 (1), 73, 2009 | 49 | 2009 |

A practical decision procedure for propositional projection temporal logic with infinite models Z Duan, C Tian Theoretical Computer Science 554, 169-190, 2014 | 45 | 2014 |

Model checking propositional projection temporal logic based on SPIN C Tian, Z Duan International Conference on Formal Engineering Methods, 246-265, 2007 | 42 | 2007 |

Expressiveness of propositional projection temporal logic with star C Tian, Z Duan Theoretical computer science 412 (18), 1729-1744, 2011 | 41 | 2011 |

Propositional Projection Temporal Logic, Bchi Automata and *ω*-Regular ExpressionsC Tian, Z Duan International Conference on Theory and Applications of Models of Computation …, 2008 | 36 | 2008 |

How Android App Developers Manage Power Consumption?-An Empirical Study by Mining Power Management Commits L Bao, D Lo, X Xia, X Wang, C Tian 2016 IEEE/ACM 13th Working Conference on Mining Software Repositories (MSR …, 2016 | 25 | 2016 |

Model checking concurrent systems with MSVL N Zhang, Z Duan, C Tian Science China Information Sciences 59 (11), 1-3, 2016 | 24 | 2016 |

Making CEGAR more efficient in software model checking C Tian, Z Duan, Z Duan IEEE Transactions on Software Engineering 40 (12), 1206-1223, 2014 | 24 | 2014 |

Detecting spurious counterexamples efficiently in abstract model checking C Tian, Z Duan 2013 35th International Conference on Software Engineering (ICSE), 202-211, 2013 | 23 | 2013 |

Towards more accurate content categorization of API discussions B Zhou, X Xia, D Lo, C Tian, X Wang Proceedings of the 22nd International Conference on Program Comprehension …, 2014 | 22 | 2014 |

A cylinder computation model for many-core parallel computing N Zhang, Z Duan, C Tian Theoretical Computer Science 497, 68-83, 2013 | 22 | 2013 |

An efficient approach for abstraction-refinement in model checking C Tian, Z Duan, N Zhang Theoretical Computer Science 461, 76-85, 2012 | 20 | 2012 |

A canonical form based decision procedure and model checking approach for propositional projection temporal logic Z Duan, C Tian, N Zhang Theoretical Computer Science 609, 544-560, 2016 | 19 | 2016 |

A mechanism of function calls in MSVL N Zhang, Z Duan, C Tian Theoretical Computer Science 654, 11-25, 2016 | 18 | 2016 |

MSVL: a typed language for temporal logic programming X Wang, C Tian, Z Duan, L Zhao Frontiers of Computer Science 11 (5), 762-785, 2017 | 17 | 2017 |

A compiler for MSVL and its applications K Yang, Z Duan, C Tian, N Zhang Theoretical Computer Science 749, 2-16, 2018 | 14 | 2018 |

Full regular temporal property verification as dynamic program execution M Wang, C Tian, Z Duan 2017 IEEE/ACM 39th International Conference on Software Engineering …, 2017 | 12 | 2017 |

Model checking C programs with MSVL Y Yu, Z Duan, C Tian, M Yang International Workshop on Structured Object-Oriented Formal Language and …, 2012 | 12 | 2012 |