“无穷字母表上的形式模型：逻辑与自动机”, 国家自然科学基金青年基金, 2012-2014，主持.

  “符号模型与隐式模型检测技术”, 国家自然科学基金面上基金, 2013-2016，参与（主持： 张文辉研究员 ）.