1976-1978福建宁德地区民族中学

1978-1979北京大学

1979-1988挪威奥斯陆大学

1986-1986挪威INENCO公司

1987-1987挪威奥斯陆大学

1988-1989中科院软体所

1989-1989香港Citibank公司

1989-1991挪威奥斯陆大学

1991-1993挪威Telemark学院

1993-1994中科院软体所

1994-1995挪威Telemark学院

1995-1997挪威Achilles公司

1997-2001挪威能源技术研究所

2001-2004中科院软体所

主要从事形式化方法及相关领域的研究，在程式的形式验证、逻辑推理、模型检测、软体系统设计方法的形式化等方面有一定的研究积累。在自动推理的研究方面，对谓词公式中的量词和其它逻辑联结词作了详细的分析。区分了引理中它们的使用对证明的複杂性的不同影响。在这基础上分析了连线法和消解法及其变种与可自由使用引理的逻辑系统的关係，论证了这些方法在引理使用上的不同的局限性，加深了对自动定理证明方法的不足的认识，并揭示了扩展的消解法，即允许表示定义的重言子句集合加到初始子句集合进行消解，其功能实质上就是为了增加複杂引理套用的可能性，以提高推理效率。在这些工作的基础上，提出了一个分析模型个数的算法和一个命题逻辑公式判定的算法，取得了良好的理论效果。这方面的工作对认识自动定理证明的困难本质和命题逻辑公式判定算法的研究起到了一定的推动作用。在模型检测的研究方面，将模型检测方法套用于操作程式的验证，提出了多种针对具体套用做抽象和分不同情况以降低模型检测空间和时间複杂性的方法，包括将操作程式和操作环境的模型用中间进程分开，递增式地对操作环境进行建模和逐级验证以降低模型检测的套用门槛；基于对套用目标和模型的分析，将套用领域的特殊性质嵌入到模型及性质描述中以降低模型检测的複杂性；结合对模型的静态分析，将所选的不同情况嵌入到性质描述中以降低模型检测的複杂性。这方面的工作对模型检测在不同领域的套用有一定的借鉴作用。

1993年获王宽诚科研奖金资助

2002年获财政部中科院引进国外杰出人才资助