当前位置：文档之家 › 中科大-耶鲁高可信软件联合研究中心

中科大-耶鲁高可信软件联合研究中心

  • 格式：doc
  • 大小：40.00 KB
  • 文档页数：3

下载文档原格式

  / 3

合集下载

中科大考博辅导班：2019中科大计算机科学与技术学院考博难度解析及经验分享

中科大考博辅导班：2019中科大计算机科学与技术学院考博难度解析及经验分享

中科大考博辅导班：2019中科大计算机科学与技术学院考博难度解析及经验分享中国科学院大学2019年博士研究生招生统一实行网上报名。

报考者须符合《中国科学院大学2019年招收攻读博士学位研究生简章》规定的报考条件。

考生在报考前请联系所报考的研究所(指招收博士生的中科院各研究院、所、中心、园、台、站)或校部相关院系，了解具体的报考规定。

下面是启道考博辅导班整理的关于中国科学技术大学计算机科学与技术学院考博相关内容。

一、院系简介中国科技大学于1958年建校时就设置了计算机专业，老一辈计算机科学家夏培肃先生等亲自执教，创办之初，与中科院计算所合作自主设计并研制成功了我国第1台通用计算机--107机并于1960年安装于中国科大、1975年研制成功小型机KD-3，1983年与中科院计算所联合研制成功了功能分布式阵列处理机系统GF10系列，1983年研制成功了微型机KD-4和KD-5并于次年转让给湖北无线电二厂投入生产。

1982年成立了计算机科学技术系, 与中科院计算所联合培养了国内首批博士。

1990年获得计算机软件博士学位点；1995年成立了我国的第1个国家高性能计算中心；2000年获计算机科学与技术一级学科博士学位授予权，并建立博士后流动站，该学科是中国科学院博士生重点培养基地；2007年我系计算机软件与理论专业经教育部评审为国家重点学科。

2009年3月计算机科学与技术学院正式成立。

本着"全院办校,所系结合"的办校方针,我院和中国科学院计算所、软件所、沈阳自动化所对口结合。

二、招生信息中国科学技术大学计算机科学与技术学院博士招生专业有2个：081200计算机科学与技术研究方向：1．机器学习与大数据分析．大数据的并行存储与处理．面向认知问题的可重构计算．并行程序设计与优化．超大规模并行计算机系．个性化推荐．社交网络分析．并行算法．高性能计算及应用．机器学习．数据挖掘．计算智能．网络通信，网络安全，计算机互连网络．并行和分布式处理，网络计算．系统与软件优化，代码优化．机器学习与大数据处理．网络科学．信息安全．高性能计算及应用．边缘计算．分布式一致性理论及其应用．大规模、实时、高可靠分布式存储系统．面向智能计算的系统软件．软件工程．分布式系统．数据共享，交易和大数据分析．无线网络及物联网．网络和信息安全．赛博经济学．网络科学．机器学习与随机建模．大规模存储系统．车联网．下一代无线网络．计算机应用技术．高可信软件．程序设计语言及编译．操作系统．计算机图形学．计算机视觉．大数据管理与分析．数据库与智能信息检索．空间数据库与基于位置的服务．数据挖掘．互联网搜索．数据挖掘．人工智能．城市计算．移动计算．网络与信息安全．移动计算安全．大数据挖据与计算．并行计算与性能优化．高性能计算及应用．存储系统．物联网安全．智能感知与通信．可穿戴计算．移动计算．机器学习和大数据分析．信息安全和隐私保护．无线网络．智能电网．基于深度学习的大数据分析．智能处理器．可重构系统．分布式系统085271电子与信息研究方向：不区分研究方向三、报考条件（1）中华人民共和国公民；拥护中国共产党的领导，愿意为祖国社会主义现代化建设服务；品德良好，遵纪守法，学风端正，无任何考试作弊、学术剽窃及其它违法违纪行为；（2）身体健康状况符合我校规定的体检要求，心理正常；（3）申请者原则上应来自国内重点院校或所在高校学习专业为重点学科；（4）专业基础好、科研能力强，在某一领域或某些方面有特殊学术专长及突出学术成果；（5）对学术研究有浓厚的兴趣，有较强的创新意识、创新能力和专业能力；（6）申请者的学位必须符合下述条件之一：应届硕士毕业生须在博士入学前取得硕士学位；或已获得硕士或博士学位；在境外获得学位的考生，须凭教育部留学服务中心的认证书报名；（7）具有较强的语言能力，外语（限本单位招生专业目录中公布的语种）水平较高。

学生生涯规划指导资料

学生生涯规划指导资料

近年北京理工大学录取分数线
浙江理科
重点线
550 568 570 550
满分 750 必修 +60 模块选修
★ 一级学科国家重点学科（4个） · 机械工程 · 光学工程 · 信息与通信工程 · 兵器科学与技术 ★ 二级学科国家重点学科（5个） · 工程力学 · 动力机械及工程 · 物理电子学 · 控制理论与控制工程 · 应用化学
中文名：上海外国语大学 简称：上外(SISU) 校训：格高志远 学贯中西 创办时间：1949年12月 类别：公立大学 学校类型：语言 主管部门：教育部 学校属性：211工程 所属地区：中国上海 主要院系：英语学院，新闻传播学院，俄语 系，德语系，国际工商管理学院 硕士点：23个 博士点：10个
带Y者为第十次增列学位点或2006年新增专业学位点 国家重点学科 英语语言文学 俄语语言文学 一级学科博士点 外国语言文学 博士点 国际关系 一级学科硕士点 外国语言文学 新闻传播学 Y 硕士点 国际贸易学 国际政治 Y 国际关系 外交学 思想政治教育 Y 教育技术学 语言学及应用语言学 中国现当代文学 比较文学与世界文学 企业管理
机械电子工程 本学科点１９５５年开始培养研究生，１９８６年批准有权授予博 士学位，并设有博士后流动站。１９９２年批准建立“机电工程与 控制国家级重点实验室”，２００２年被批准为国家级重点学科。 本学科点已形成由我国著名引信技术专家马宝华教授、传感与测控 技术专家李科杰教授为学科带头人，以２２名教授（１０名博士生 导师）为学术带头人和骨干、共计５６名教学、科研人员组成的高 素质学术队伍。以机电工程与控制国家级重点实验室，机器人、数 控与检测、机电一体化和微小型系统研究中心为研究基地，仪器及 设备总价值约７０００万元。本学科“九五”以来承担了上百项国 家项目。“十五”期间，研究总经费共计数千万元。“九五”以来 共获得国家奖五项、部级科技奖数十项。 本学科为国家培养了一大批高层次专门技术人才，目前每年招收３ ０余名博士生、１００余名硕士生以及１５０余名本科生。 本学科的综合实力和教学、科研水平在我国同类学科中名列前茅。

证明辅助工具Coq简介

证明辅助工具Coq简介
Inductive EqNat : nat -> nat -> Prop := | OEq : EqNat O O | SEq : forall m n : nat, EqNat m n -> EqNat (S m) (S n).
四色定理
• G. Gonthier & B. Werner • 2004年证明
• 证明？ • 完整详细的Coq证明 • 机器可检查 • 没有跳过任何步骤 • 证明检查程序规模小
高可信软件
• 嵌入式系统内核——seL4 • G. Klein 等人 • OSDI’09 Best Paper • 8700 lines of C • 经过形式化验证
• 证明？ • 机器可检查证明 • 200,000 lines of Isabelle script
VeriSoft
• 芯片 • 嵌入式内核
• 汽车电子控制单元 • 应用
• 宝马汽车的应急呼叫系统 • 证明：
• Isabelle 2005
CompCert
• 经过完全证明的C语言编译器 • Xavier Leroy [CACM ’09] • Power PC backend
归纳谓词
• 问题：证明 EqNat 0 0 ? • 写出类型为EqNat 0 0的证明构造
• 答案： OEq
Lemma LEqNat1 : EqNat O O. Proof OEq. Definition LEqNat1 : E明 EqNat 1 1 ? • 写出类型为EqNat 1 1的证明构造
运行 Coq
• 运行 coqtop
• 检查一个表达式的类型 Coq< Check 3.
3 : nat
Coq< Check 3 + 5.

中国科学院软件研究所2019年统考硕士拟参加复试考生名单公示

中国科学院软件研究所2019年统考硕士拟参加复试考生名单公示

中国科学院软件研究所2019年统考硕士拟参加复试考生名单公示考生编号考生姓名报考专业代码毕业学校名称初试总分复试分组备注144309150000001 李明慧083500 华北电力大学404 A组144309150000146 许润清081202 华中科技大学382 A组144309150000067 康嘉文081202 大连理工大学381 A组144309150000055 李序083500 河北地质大学363 A组144309150000160 谭四君083500 上海交通大学361 A组144309150000029 李勰081202 中国科学院大学353 A组144309150000124 刘浩081202 西安电子科技大学352 A组144309150000024 胡登杭081202 中国科学院大学351 A组144309150000038 王化磊081202 中国民航大学350 A组144309150000037 李晴081203 天津工业大学347 A组144309150000091 李仞珏081202 常州工学院347 A组144309150000068 张宠081202 大连理工大学346 A组144309150000116 韩明钦081202 山东大学345 A组144309150000175 张震083500 西北工业大学341 A组144309150000044 李婷081202 东北大学331 A组144309150000117 赵志鹏081202 山东科技大学326 A组144309150000161 谢异081202 上海交通大学385 B组144309150000042 李蕴辉083500 南开大学383 B组144309150000168 熊轶翔083500 太原理工大学383 B组144309150000033 徐可钦081202 北京科技大学375 B组144309150000077 吕泽081203 吉林大学348 B组144309150000118 王舰081203 山东科技大学346 B组144309150000016 汪钇丞081202 中国科学院大学342 B组144309150000066 蒋筱斌083500 大连理工大学342 B组144309150000051 赵新朋081203 大连理工大学339 B组144309150000026 黄智榕083500 北京科技大学330 B组144309150000050 郑超081202 河北工业大学329 B组144309150000049 李梦晗081202 中国科学技术大学326 B组144309150000070 刘晓航083500 东北大学325 B组144309150000074 孙业程081203 吉林大学325 B组144309150000152 吴雨浩085212 华中科技大学404 C组144309150000088 王伟085212 南京农业大学396 C组144309150000030 王可085212 中央财经大学380 C组144309150000119 董柯085212 山东科技大学379 C组144309150000113 陈子轩085212 山东中医药大学370 C组144309150000021 桑倩085212 中央财经大学356 C组144309150000053 张帅085212 大连理工大学356 C组144309150000098 恽星彤085212 沈阳农业大学356 C组144309150000121 薄震强085212 青岛科技大学339 C组144309150000159 程梦琪085212 湖南师范大学328 C组144309150000133 魏松江085212 南华大学325 C组144309150000154 张炜085212 中南大学325 C组144309150000162 伊力夏提·图尔荪085212 中山大学323 C组专项144309150000060 李旭然085212 长安大学322 C组专项。

计算机体系结构国家重点实验室(中国科学院计算技术研究所)

计算机体系结构国家重点实验室(中国科学院计算技术研究所)

组织结构
为求解计算机领域的上述重大科学问题，同时面向长远的科学发展需求，计算机体系结构国家重点实验室设 立五个主要研究方向，即计算机系统、微体系结构、编译和编程、VLSI与容错计算、非传统计算机体系结构。围 绕五个研究方向，结合实验室现有的基础和未来的发展规划，进一步分为四个实验室和四个研究组：先进计算机 系统实验室、微体系结构实验室、编译与编程实验室、集成电路实验室、并行算法研究组、处理器设计研究组、 存储系统研究组、量子计算研究组。
发展目标
建立具有国际水平的计算机体系结构研究实验平台，为全国计算机体系结构研究提供基础支持，为提高我国 计算机体系结构整体研究水平作出贡献。建设一支高水平、跨学科、结构合理的研究队伍，将学术骨干培养成为 所在研究领域中享有国际声誉的科学家，在国际上代表国内最高水平，建立计算机体系结构领域国际一流的科学 研究、技术创新和人才培养的基地。以满足高性能计算、高通量计算和人机物三元融合的计算需求为突破口，研 究万亿次级芯片体系结构，构建艾级（更高）高性能计算机；研究千线程级芯片体系结构，构建千万线程级高通 量计算机；发展可重塑芯片和族群体系结构，构建海云计算融合新型计算模式。进行面向艾级计算、EB级数据、 亿级并行的基础研究，研制50GF/w原型系统，突破2020技术墙。具体包括：单芯片百瓦、千核、十万亿次的处理 器体系结构设计、测试验证和自修复方法；十万个处理器芯片构成的系统互连和容错方法；亿级并行度的编程和 算法设计方法；高端计算如何利用新工艺、新器件（3D封装、光互连）的最新成果。
计算机体系结构国家重点实验室（中 国科学院计算技术研究所）
计算机体系结构国家重点实验室
01 基本信息
03 研究方向 05 组织结构
目录
02 正式揭牌 04 发展目标 06 研究单元

计算机科学国家重点实验室(中国科学院软件研究所)

计算机科学国家重点实验室(中国科学院软件研究所)

研究领域
实验室以国内外计算机科学技术领域提出的基本问题为背景，面向国家发展软件产业和国家安全的战略需求， 开展计算机科学理论和软件基础研究。
招生指南
实验室每年面向国内外招收有志于在计算机科学方面追求卓越的硕士、博士研究生和博士后，也面向青年学 子招收部分实习生。实验室招生基本要求：有坚实的数学基础，有优良的算法设计与编程实验能力，有良好的英 文交流能力，有团队合作精神。热忱欢迎计算机科学与技术、软件工程与多媒体，以及数学、物理、自动控制等 相关学科的学生加盟。
交流合作
实验室积极开展各种形式的学术交流和与国内外同行的合作。实验室积极邀请国内外知名学者来访进行学术 交流。每年有数十位从事计算机科学基础研究的国际同行来访交流；访问过实验室的计算机科学最高奖图灵奖获 得者有Juris Hartmanis、Tony Hoare、Robin Milner、Amir Pnueli、Andrew Yao、John Hopcroft、 Joseph Sifakis、Edmund Clarke、Allen Emerson、Leslie Valiant。实验室已经成为国际同行了解我国计 算机科学基础研究水平的重要窗口和建立的桥梁。
建议参加复试的学生在与上述要求相关的课程方面多作准备，如高等数学、线性代数、离散数学、数据结构、 算法分析与设计等。
学术团队
实验室现有研究人员50人，其中中国科学院院士3人，博士生导师24人，55岁以下的研究人员均有博士学位， 形成了一个以中青年为主体、思想活跃、充满朝气的群体。实验室成员已获得国家自然科学奖一等奖1项、二等奖 2项，国家科技进步奖二等奖5项等奖励。在中科院和软件所的领导与支持下，实验室全体成员共同努力，在科学 研究和队伍建设方面做了大量的工作，承担了多项国家和科学院的重大重点项目。实验室坚持把研究的质量和水 平放在首位，自觉抵制急功近利、浮躁虚夸的不良风气，同时提倡学术民主，鼓励不同学术观点的竞争与融合。 实验室有多位我国计算机软件科学事业的奠基人和开拓者。

智能制造工程训练中心方案

智能制造工程训练中心方案目录一、前言 (3)1.1 编写目的 (3)1.2 背景与意义 (4)二、总体目标与建设内容 (5)2.1 总体目标 (7)2.2 建设内容 (7)2.2.1 硬件设施建设 (9)2.2.2 软件系统建设 (10)2.2.3 人才队伍建设 (11)三、功能定位与业务范围 (12)3.1 功能定位 (14)3.2 业务范围 (15)3.2.1 人才培养 (16)3.2.2 科研创新 (17)3.2.3 社会服务 (20)四、教学计划与课程设置 (21)4.1 教学计划 (21)4.2 课程设置 (23)4.2.1 基础课程 (24)4.2.2 专业课程 (26)4.2.3 实践课程 (28)五、教学方法与手段 (29)5.1 教学方法 (30)5.1.1 项目式教学 (31)5.1.2 问题导向学习 (32)5.1.3 翻转课堂 (33)5.2 教学手段 (35)5.2.1 现代教育技术应用 (36)5.2.2 实训基地建设 (37)六、师资队伍与培训 (39)6.1 师资队伍 (40)6.1.1 人才引进 (41)6.1.2 培训提升 (42)6.2 培训计划 (43)6.2.1 入职培训 (44)6.2.2 在职培训 (45)七、运营管理与评估 (46)7.1 运营管理 (48)7.1.1 制度建设 (49)7.1.2 运行监控 (50)7.2 评估体系 (51)7.2.1 教学质量评估 (52)7.2.2 设备设施评估 (53)八、发展规划与政策建议 (55)8.1 发展规划 (56)8.2 政策建议 (57)8.2.1 资金支持政策 (58)8.2.2 人才引进政策 (59)九、结语 (61)一、前言随着全球经济的快速发展和科技的不断进步，制造业作为国民经济的主体，其转型升级已成为各国政府和企业共同关注的重点。

智能制造作为制造业发展的主要趋势，正引领着一场前所未有的产业变革。

软件开发环境国家重点实验室

软件开发环境国家重点实验室软件开发环境国家重点实验室简介软件开发环境国家重点实验室于1988年通过国家计委专家认证，并确定为用世界银行贷款建设的国家重点实验室。

1992年后获得世界银行贷款共129万美元，购置了实验室建设初期的要紧设备与基础设施，1992年10月对外开放。

1995年通过了教育部与基金委组织的专家验收。

实验室是国家对外开放的软件新技术、软件开发工具与环境的应用基础研究与关键技术研发基地。

实验室实行主任负责制与学术委员会评审制。

国务院学位委员会委员、中国科学院院士、北京航空航天大学校长李未教授担任实验室主任。

1997年12月经教育部批准，成立了第二届学术委员会，由12名国内外知名专家构成，中国科学院院士董韫美教授担任主任。

本届学术委员会成员中的二位外籍专家，分别来自日本筑波大学与德国马普计算机研究所。

1996年以来，实验室基于对软件产业国际国内形势的分析，确定了“面向软件产业进展的主战场，瞄准软件基础研究的世界前沿，突破研制大型软件的关键技术，深化原创性的软件基础研究”的进展战略。

在这个进展战略的指导下，实验室根据自身多年的学术积存与研究特色，并结合国际学科前沿研究与进展趋势，以原创性理论研究为基础，以关键技术突破为重点，以研制先进的软件开发环境与平台为总目标，设立了计算机科学理论与基础、高速网下的协同工作环境与面向领域服务的软件支撑技术三个有特色、有优势的研究方向。

自1996年以来，实验室共承担科研项目共156项。

其中，国家科学基金项目14项，攀登计划（子课题）1项，973计划项目1项（4个课题），863计划项目23项，部委级重点项目11项，其他课题及横向协作项目94项,科研经费共计8065万元。

实验室取得的要紧成果有：在软件基础研究方面：1）在国内率先倡导将网络环境下海量信息的组织、传输与处理的研究作为软件基础研究的一个重要方向，并制定了全面的研究计划。

1999年科技部重大基础研究规划项目“网络环境下海量信息的组织、处理与传输的理论与方法”正式立项启动，实验室主任李未院士任该项目的首席科学家。

第一批-中国科学技术大学教务处

2010年夏季学期课程公布（第一批）：大师系列课程（国内外大师、所系结合前沿讲座等）：生命学院：三维显微术与科学前沿（英语授课）40学时 2学分上课时间：8月4日——8月18日任课教师：周正洪、毕国强面向对象：全校本科生、研究生课程简介：三维显微术（包括激光共聚焦，冷冻电镜三维重构，原子力显微术）在现代生物学，结构生物学和生物医学研究中起着关键性的作用。

本课程主要介绍各种显微术的原理和应用，重点讲述三维结构重建。

授课对象包括生物学、物理学、计算机科学等专业高年级本科生和研究生。

计算机学院：演化计算20学时 2学分考核方式：课程报告上课时间: 2010年8月18日至22日，18日下午3学时、19日上午3学时、19日下午3学时、20日上午3学时、20 日下午3学时、21日下午3学时、22日上午2学时（具体的时间可能会需要微调）。

任课教师: 姚新（伯明翰大学教授，我校大师讲席教授）面向对象: 全校高年级本科生。

预修课程：人工智能、概率论与数理统计、随机过程等相关课程。

课程简介：演化计算是一个新兴的前沿交叉学科。

作为一种问题求解方法，演化计算技术在求解非连续、不可微、多峰、以及目标函数难以定义的问题时，表现出较大的性能优势，被广泛应用于许多实际问题的求解。

本课程将系统介绍演化计算的基础知识、常见演化计算模型的工作原理、演化算法的性能分析方法，并通过应用实例讲解演化计算方法的使用方法与实现技巧。

可信软件的前沿理论和技术21/28学时 2学分考核方式：课程实践方式上课时间：7月19日——7月25日，连续7天。

上午3学时理论课，下午4学时实践课任课教师：理论课教师：邵中（耶鲁大学教授，我校大师讲席教授）、陈意云（中科大教授）实践课助教：中科大－耶鲁高可信软件联合中心博士生面向对象：计算机科学与技术、数学、信息安全或相关专业的本科生预修课程：程序设计、数据结构课程简介：本课程介绍高可信软件研究领域中国际前沿的理论、技术和热点课题，涉及系统内核的验证、应用程序的验证、出具证明的编译器、程序验证中的自动定理证明技术等方面，并通过由浅入深地指导学生用国际流行的证明辅助工具来验证一些简单的程序，让学生更好地理解相关的理论和技术。

基于大模型的具身智能系统综述

基于大模型的具身智能系统综述目录1. 内容概要 (2)1.1 研究背景 (2)1.2 具身智能系统的概念 (4)1.3 大模型在具身智能中的应用 (5)2. 具身智能系统的发展历程 (7)2.1 早期研究 (8)2.2 现代研究 (10)2.3 未来发展趋势 (11)3. 大模型在具身智能系统中的应用 (13)3.1 模型选择 (14)3.2 数据处理与生成 (15)3.3 模型训练与优化 (17)3.4 应用实例 (19)4. 具身智能系统的关键技术 (21)4.1 感知与理解 (22)4.2 运动规划与控制 (23)4.3 多模态交互 (25)4.4 自主学习与适应 (26)5. 应用领域 (27)5.1 医疗领域 (29)5.2 教育领域 (30)5.3 服务业 (32)5.4 制造业 (33)6. 面临的挑战与未来展望 (34)6.1 安全性与隐私 (36)6.2 成本与资源消耗 (37)6.3 道德与社会影响 (39)6.4 技术合作与发展 (39)1. 内容概要随着人工智能技术的迅猛发展，大模型及具身智能系统逐渐成为研究热点。

本综述旨在全面、深入地探讨基于大模型的具身智能系统的研究现状、技术挑战与未来发展方向。

我们将回顾大模型在具身智能系统中的应用背景和基本原理，包括强化学习、知识蒸馏等关键技术在大模型上的应用。

我们将重点分析当前具身智能系统的最新进展，如自动驾驶、智能机器人等领域的实践案例，并从感知、决策、控制等方面评估其性能。

我们还将讨论大模型具身智能系统面临的主要技术挑战，如数据质量、模型泛化能力、计算资源限制等问题。

针对这些挑战，我们将提出可能的解决方案和未来研究方向。

我们将展望具身智能系统的未来发展趋势，包括跨模态融合、多智能体协同、隐私保护等方面的探索。

通过本综述，我们期望为相关领域的研究人员和工程技术人员提供有价值的参考信息，共同推动具身智能系统的进步与发展。

1.1 研究背景随着人工智能和机器学习领域的迅猛发展，特别是深度学习技术和大模型的广泛应用，智能系统的能力得到了极大的提升。

  1. 1、下载文档前请自行甄别文档内容的完整性，平台不提供额外的编辑、内容补充、找答案等附加服务。
  2. 2、"仅部分预览"的文档,不可在线预览部分如存在完整性等问题,可反馈申请退款(可完整预览的文档不适用该条件!)。
  3. 3、如文档侵犯您的权益，请联系客服反馈,我们会尽快为您处理(人工客服工作时间：9:00-18:30)。

中科大－耶鲁高可信软件联合研究中心
简介
一、概述
在中科大软件安全实验室和耶鲁大学FLINT实验室近五年合作的基础上，双方校长于2008年10月签署备忘录，以中科大软件安全实验室为基础，在中科大建立高可信软件联合研究中心。

该中心是在两校相关实验室多年合作的基础上建立的。

五年多来，我校软件安全实验室在耶鲁大学邵中教授的指导（包括和他主持的FLINT实验室的合作）下，研究水平上升较快。

在邵中教授的支持下，软件安全实验室多次获得国家基金面上项目的资助，目前正在合作申请“海外及港澳学者合作研究基金”。

在国际会议和国内外期刊上，两校研究生共同发表了7篇论文，我校研究生单独发表论文10多篇。

近6年在编程语言理论及实现技术、软件安全和软件形式验证等研究方向培养了18名博士，其中在高校当教师的有8人，在Intel、Microsoft和Sun公司研发部门工作的有6人，做博士后的有2人。

二、研究领域
（1）程序设计语言理论和实现技术。

这是一个持续活跃了半个世纪的研究领域，目前国际上最活跃的方向是并行编程语言的设计和实现技术、程序验证技术等。

我们目前的研究集中在形式程序验证（formal program verification）和出具证明编译器（certifying compiler）两个方向上。

通过近几年的国际合作研究，研究水平上升较快。

（2）第2步拟展开的研究方向是计算机网络方面。

有待耶鲁大学相关教授来访，和华蓓教授（可见htttp:///~bhua）和董群峰教授等经过充分交流后展开。

在高可信软件研究领域，联合研究中心以形式程序验证为主要方法，研究提高软件可信程度的理论和技术等，目前正在开展的课题有系统软件的形式验证、出具证明的编译器技术、并发多核软件的开发、自动定理证明系统等在高可信软件研究领域，联合研究中心近5年的建设目标是：研究如何有效地集成形式程序验证和领域专用语言和逻辑（domain-specific languages and logics）这两种软件技术，形成提高编写高可信软件生产力、提高对它们正确性和安全性信任程度、并且能被工业界接受的软件开发新方法，构建基于此方法并能向工业界推广的开发携带证明大型系统软件的基础结构。

这是一项为了把形式程序验证技术推向实用，解决其中理论和技术问题的奠基性研究。

这项研究的成果将对提高安全攸关软件的可信度，对建设各种安全的信息系统有着重要作用。

三、研究团队
1、研究人员
目前在高可信软件及相关领域的研究人员如下：
∙教授：邵中、陈意云、华蓓、董群峰、冯新宇
∙副教授：张昱
∙博士后：郭宇、李兆鹏、付明
∙博士：华保健、郭燕
∙博士生和硕士生：20名左右
四、在高可信软件领域中的合作成果
1、近5年连续承担国家自然科学基金面上项目：
∙基于语言理论和实现技术的移动代码安全（Security of mobile code based on techniques of programming language theory and implementation）
∙类型论在软件安全方面的应用研究（Application Research of Type Theory in Software Security and Safety）
∙软件安全性的验证和编译（Verification and Compilation of Software Safety）∙面向携带证明软件设计的语言、逻辑和证明（Languages, Logics, and Proofs for Certified Software Design）
2、近5年在编程语言理论及实现技术、软件安全和软件验证方面培养了14名博士，其中在Intel、Microsoft和Sun等公司研发部门工作的有6人，在高校当教师的有6人，做博士后的有2人。

3、近期发表的代表性论文如下：
[1] X. Feng, Z. Shao, A. Vaynberg, S. Xiang, and Z. Ni. Modular verification of assembly code with stack-based control abstractions. In Proc. 2006 ACM Conference on Programming Language Design and Implementation, pages 401-414, June 2006. [2] Chunxian Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, and Yu Guo. Foundational typed assembly language with certified garbage collection. In Proceedings of 1st IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, pages 326-335, IEEE CS press, June 2007.
[3] X. Feng, Z. Ni, Z. Shao, and Y. Guo. An open framework for foundational proof-carrying code. In Proc. 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation, pages 67-78, Jan. 2007.
[4] A. McCreight, Z. Shao, C. Lin, and L. Li. A General Framework for Certifying Garbage Collectors and Their Mutators. In Proc. 2007 ACM Conference on Programming Language Design and Implementation, pages 468-479, June 2007. [5] X. Feng, Z. Shao, Y. Dong, and Y. Guo. Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. In Proc. 2008 ACM Conference on Programming Language Design and Implementation, pages 170-182, June 2008. [6] X. Feng, Z. Shao, Y. Guo and Y. Dong. Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. In Proc. Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments, October 2008.
五、欢迎加入联合研究中心
随着联合研究中心的正式成立，研究生导师、博士后和博士研究生的队伍都会逐步扩大。

欢迎对联合研究中心研究领域感兴趣的同学加入中心攻读博士学位。

经中国科学技术大学有关部门同意，联合研究中心面向国内外公开招聘研究生导师。

招聘条件如下：
教授：具有博士学位，年龄不超过45周岁，在本领域取得了国内外同行所公认的学术成果，有指导博士研究生的能力。

副教授：具有博士学位，年龄不超过40周岁，有较大发展潜力，在本领域取得了一定的学术成绩，有指导研究生的能力。

招聘流程按照中国科学技术大学的规定，中国科学技术大学提供有竞争力的工作报酬和条件。

应聘者将个人简历、研究工作陈述和3位国内外同行专家推荐函，通过电子邮件发到kyhcs@。

联合研究中心经初步筛选后，推荐优秀者进入中国科学技术大学招聘流程。

此外，联合研究中心还招收博士后：年龄不超过35岁，在本领域取得了初步的学术成绩。