Students

Ph.D.

  • (2007) Jin Yi: Büchi自动机状态空间的化简(State Space Reduction of Buchi Automata)
  • (2007) Zhilin Wu: 时序逻辑理论研究:表达能力和复杂性(On the theoretical Aspects of Temporal Logics: Expressive Power and Complexity)
  • (2008) Syed Asad Raza Kazmi: Intuitionistic Linear-time mu-Calculus
  • (2009) Hongtao Huang: 分布式系统中必然方式下谓词检测的研究(Predicate Detection under Definitely Modality in Distributed Systems)
  • (2009) Xiang Zhou: 特定类有穷结构上的逻辑的表达能力(Expressive Power of Logics on Special Classes of Finite Structures)
  • (2009) Yanyan Xu: 基于BDD的增量启发式搜索方法及其应用(BDD-based Incremental Heuristic Search and Its Applications)
  • (2009) Liang Xu: 限界模型检测方法及其应用(Bounded Model Checking and Its Applications)
  • (2010) Wei Chen: 关于可满足性问题的一些研究及其在模型检测中的应用(Problems in Satisability Solving and Applications in Model Checking)
  • (2013) Teng Long: 公平性约束下基于抽象和推理的活性验证(Liveness Verication by Abstraction and Deduction under Fairness)
  • (2014) Naiju Zeng: SystemC程序的形式化验证方法研究(Formal Verication of SystemC Programs)
  • (2017) Zhaowei Xu: 程序验证的理论和方法(Theories and methods of Program Verification)
  • (2020) Ran Chen: 多智能体系统的形式验证方法研究(Verification of Multi-agent Systems)

    M.Sc.

  • (2009) Jinxiu Du: 基于SAT的LTL限界模型检测与验证
  • (2009) Weisong Li: 弱互模拟等价类算法改进
  • (2009) Qingkui Feng: 基于一阶迁移系统的限界模型检测工具实现
  • (2009) Xiaoliang Wang: 基于Yices对时间自动机的有界模型检测
  • (2010) Shaochun Wang: 卫命令模型检测工具的设计与实现
  • (2013) Lanlan Zhang: 基于Verds的C语言子集模型检测方法研究
  • (2016) Jing Ma: AKC攻击的模式、预防及案例分析
  • (2022) Ya Gao: 多智能体自动机及其在时序认知逻辑验证上的应用

    Misc

  • Bai Su
  • Wang Qi
  • Yu Tingting
    Some Papers by Students

    Zhaowei Xu, Taolue Chen, Zhilin Wu. Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints. CADE 2017: 509-527.

    Shaochun Wang. Temporal Filter: A Temporal Extension to Wireshark Display Filter (Short paper). SEKE 2010:421-424.

    Yanyan Xu, Weiya Yue, Kaile Su. The BDD-Based Dynamic A* Algorithm for Real-Time Replanning. LNCS 5598 (FAW 2009):271-282.

    Yanyan Xu and Weiya Yue. A generalized framework for BDD-based replanning A* search. SNPD 2009:133-139.

    Xiang Zhou. CFI Construction and Balanced Graphs. LNCS 5598 (FAW 2009): 97-107.

    Weisong Li. Algorithms for Computing Weak Bisimulation Equivalence. TASE 2009:241-248.

    Hongtao Huang. On Detecting of Regular Predicates in Distributed Systems. LNCS 5799 (ATVA 2009):397-411.

    Hongtao Huang. Detection of a Set of States in Distributed Systems. APSEC 2008:281-288. 2008.

    Xiang Zhou. Ehrenfeucht-Fraisse Games in Finite Set Theory. Information Processing Letters 108:3-9. 2008.

    Liang Xu. SMT-Based Bounded Model Checking for Real-Time Systems (Short Paper). QSIC 2008:120-125. 2008.

    Hongtao Huang. Detection of Disjunctive Normal Form Predicate in Distributed Systems. ICDCN 2008:158-169. 2008.

    Zhilin Wu. On the Expressive Power of QLTL. ICTAC 2007:467-481. 2007.

    Zhilin Wu. A note on the characterization of TL[EF]*. Information Processing Letters 102(2-3):48-54, 2007.

    Weiya Yue, Yanyan Xu, Kaile Su. BDDRPA*: An efficient BDD-based incremental heuristic search algorithm for replanning. LNAI 4304 (AI 2006):627-636. 2006.

    Zhilin Wu. Quasi-star-free languagaes on infinite words, Acta Cybernetica 17(1):75-93, 2005.

    徐亮. 改进的以SMT 为基础的实时系统限界模型检测. 软件学报 21(7):1491-1502. 2010.

    徐艳艳, 岳伟亚. 基于BDD的增量启发式搜索. 软件学报 20(09): 2352-2366. 2009.