姓名:董渊

职称:副教授

电话:62794240

邮箱:dongyuan@tsinghua.edu.cn

主页:http://soft.cs.tsinghua.edu.cn/~dongyuan/

教育背景

工学学士 (工程力学), 清华大学, 中国, 1996;

工学硕士 (固体力学), 清华大学, 中国, 1998;

工学博士 (固体力学), 清华大学, 中国, 2001.

社会兼职

中国计算机学会: 系统软件专业委员会委员 (2009-);

IEEE: 会员 (2009-);

ACM: 会员 (2007-);

中国“LINUX国家标准工作组”: 成员代表 (2005-).

研究领域

嵌入式操作系统, 编译系统, 基于语言的可信软件;软硬件协同设计中的软件方法

研究概况

近年来,我的研究工作及成果包括:

1. 参加国家863计划“32位高性能嵌入式CPU研发”课题,提出了一种软硬件协同开发中的操作系统设计方案,并完成开发,为CPU的设计、实现、测试和运行提供支持。

2. 研究操作系统核心代码的编译支持,给出了一种自动重定向方法,基于全球最好的开源高性能编译系统Open64完成PPC32后端的编译工作,正确性和性能均达到和GCC相当的水平;同时,设计了该编译器内嵌汇编核心代码的支持方案,首次实现了非GCC开源工具为IA64、PPC32和IA32处理器编译Linux操作系统。

3. 针对操作系统(虚拟机)中中断处理、线程切换等任务的核心代码的可信问题,研究利用证明传递的编译技术解决其正确性的形式化验证。

研究课题

863课题: 支持泛在设备的协议栈及中间件 (2009-2010);

863课题: 支持可重构的编译后端自动构造技术研究 (2008-2010);

Intel公司合作项目: 云计算客户端模块间运行时优化 (2009-2010)。

奖励与荣誉

教育部中国高校科学技术二等奖: C++语言程序设计(2001);

清华大学优秀教材特等奖: C++语言程序设计 (2008);

清华大学优秀教学软件一等奖: CCBlog网站 (2008).

学术成果

[1] Kai Ren, Shengyuan Wang, Suqin Zhang: Certify Once, Trust Anywhere: Modular Certification of Bytecode Programs for Certified Virtual Machine. APLAS 2009: 275-293

[2] Shengyuan Wang, Liwei Zhang, Ping Yang: Modular Certification of Low-Level Intermediate Representation Programs. COMPSAC (1) 2009: 563-570

[3] Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong: Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. J. Autom. Reasoning 42(2-4): 301-347 (2009)

[4] Xinyu Feng, Zhong Shao, Yuan Dong, Yu Guo: Certifying low-level programs with hardware interrupts and preemptive threads. PLDI 2008: 170-182

[5] Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong: Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. VSTTE 2008: 54-69

[6] Shengyuan Wang, Yuan Dong: Improving Combinability of Petri Nets with Inheritance, Aggregation and Association. TASE 2007: 433-439

[7] Jia Chen, Shengyuan Wang, Yuan Dong, Gui-lan Dai, Yang Yang: A Functionality Based Instruction Level Software Power Estimation Model for Embedded RISC Processors. ICESS 2004: 443-448