招生、博士后计划：

	硕士生	博士生	博士后
2010年	1	1	1

研究方向：形式化方法

2010年招聘博士后人数：1人

具体研究内容包括：

[1] 限界模型检测技术与应用

[2] 软件系统模型和时序逻辑的表达能力及相关验证方法

要求：

[1] 毕业于国内外知名大学

[2] 具有较强的团队合作精神和科学严谨作风

[3] 具有较好的理论基础

可优先考虑具有以下经验者：

[1] 熟练掌握编程方法

[2] 熟悉NuSMV、Spin、Uppaal等模型检测工具

[3] 主持或参与过较大科研课题