人民网首页

--2014清华大学计算机系篇
动态消息
获奖学生风采
中国人民大学|北京大学|清华新传学院|中国传媒大学|武汉大学|复旦大学
南京大学|华中科技大学|厦门大学|中央美术学院|北京邮电大学|清华计算机系
人民网 >> 传媒 >> 传媒专题 >> 人民网奖学金 >> 清华大学计算机科学与技术系 >> 清华计算机2014

历年获奖名单

        

人民网奖学金获奖名单：
曾薇、周睿鸣、李暄、彭璟、刘建妮、杨健

人民网优秀论文获奖者名单：
一等奖：
徐厚畅 韩梅映雪 李煜申 邢天意
二等奖：
宁威  葛明宁  童渝
三等奖：
毛逸嵘     

历年获奖名单：

2013     2012    2011    2010    2009

技术奖一等奖（4）

刘云辉

基于结构化L2,1优化的多样性关键帧提取
为了能对一段短视频提供语义上有意义的表达，本文提出了一种能同时刻画可重构能力和多样性的结构化的L2,1优化模型。为了防止相似的样本被同时选中，该模型加入了互抑制惩罚项。在互抑制因子的选择方面，该模型有高度的灵活性，本文中，我们加入了视频中的时序信息来保证结果的多样性。对于本文中非凸的目标函数，我们推导出一个迭代算法，来解决这个优化问题。我们运用多个Youtube上的片段和室内的移动机器人拍摄的视频来做性能评价。实验结果明确地显示出，相比于其他当前的方法，本文的策略能使优化模型得到更加多样化的关键帧。
详细 >>

姜宇

Design of Mixed Synchronous
Today’s system-on-chip and distributed systems are commonly equipped with multiple clocks. The key challenges in designing such systems are (1) how to model multi-clocked local synchronous component, local asynchronous component, and asynchronous communication among components in a single framework, (2) how to ensure the correctness of model, and keep consistency between the model and the implementation of real system. In this paper, we propose a novel computation model named GalsBlock for the design of multi-clocked embedded system with both synchronous and asynchronous components. The computation model consists of several hierarchical compound and atom blocks communicating with data port connections. Each atom block can be refined as parallel mealy automata. The unified operational semantic and formal semantic are defined, which can be used for simulation and verification, respectively. Then, we can generate efficient VHDL code from the validated model. The size of the generated code is reduced by up to 40% compared to simulink VHDL code generator of Stateflow for a function that can be modeled by both Galsblock and Stateflow. We have developed the graphical modeling, simulation, verification, and code generation toolkit to support the computation model, and applied them in the design of a sub-system used in the train communication control according to the standard IEC-61375. Two critical bugs in the standard are detected in the model validation process, and the automatically generated sub-system according to the revised model is now used in real subway control.
详细 >>

戴惠辰

依据被动测量的链路负载均衡
研究提出了一种实时在线的流量工程方法在多条路径之间实现负载均衡，即LAMP（load adaptation based on measuring passively）. LAMP将流量从高利用率的链路转移到低利用率的链路上，转移的依据是以被动方式收集的信息，包括数据包往返时延（round trip time，RTT）和链路利用率。LAMP不需要周期性地探测网络，不需要路由器之间的大量通信，更不需要对输入的流量和网络拓扑做任何假设。评估结果表明，LAMP能够有效降低链路利用率，而且具有良好的稳定性。
详细 >>

单来祥

基于按需即时去扩展化的LTL公式到Büchi自动机直接转换算法研究
在显式状态模型检测技术领域，现实系统通常被表达成线性时序逻辑(LTL)公式，并被转换成Büchi自动机(BA)。为了提高转换的效率，当前很多转换工具使用了中间自动机，如扩展的Büchi自动机(GBA)。去扩展化就是将GBA转换成BA的过程。本文提出并实现了LTL公式到BA的直接转换算法。本文中首次提出使用一个新的标签---接受度(Acceptance Degree，)用于记录转换过程中状态和变迁上已经满足的接受条件。是给定的LTL公式中子公式的集合。根据，本文提出一种不同于经典去扩展化算法的方法---按需即时的去扩展化(On-the-fly De-generalization，)算法。算法在展开LTL公式的过程中根据需要执行，它不同于完全展开LTL公式后，再进行去扩展化的经典方法。利用算法，我们实现了LTL 公式到Büchi自动机的直接转换，不需要使用中间自动机保存转换过程中临时结果。通过使用五组常用的LTL公式和四组随机生成的LTL公式测试已有的转换工具和本文提出转换工具，实验结果显示本文提出的直接转换方法避免了传统转换算法中的多重转换步骤，降低了计算复杂度，所需的转换时间更短。
详细 >>

技术奖二等奖（2）

吴丹

DIMR：不相交多路径域间路由
域间多路径路由, 它使源AS可以使用多条路 径发送流量到同一个目的AS, 是一种有前途的技术, 可以提高带宽,提高容错性和故障的快速恢复。 但是,以前的域间多路径路由协议,往往会产生一些相交的路径, 相交的地方形成了瓶颈, 这使得他们很容易在瓶颈处形成单点故障,因此效率不高, 降低了域间流量工程或并发多径传输的效率。 在本文中,我们提出了不相交多路径域间路由(DIMR), 试图让更多的AS找到两条不相交的路径。 在这个协议中,我们提出了路径组合的概念并设计了的路径组合选择的规则。 我们评估DIMR仿真。 实验结果表明,DIMR能使90%以上的多连接AS找到两条不相交的路径。
详细 >>

沈志荣

可搜索加密机制研究与进展
随着云计算的迅速发展，用户开始数据迁移到云端服务器，以此避免繁琐的本地数据管理并获得更加便捷的服务。为了保证数据安全和用户隐私，数据一般是以密文存储在云端服务器中，但是用户将会遇到如何在密文上进行查找的难题。可搜索加密(Searchable Encryption, 简称SE)是近年来发展的一种支持用户在密文上进行关键字查找的密码学原语，它能够为用户节省大量的网络和计算开销，并充分利用云端服务器庞大的计算资源进行密文上的关键字查找。本文介绍了SE机制的研究背景和目前的研究进展，对比阐述了基于对称密码学和基于公钥密码学而构造的SE机制的不同特点，分析了SE机制在支持单词搜索、连接关键字搜索和复杂逻辑结构搜索语句的研究进展。最后阐述了其所适用的典型应用场景，并讨论了SE机制未来可能的发展趋势。
详细 >>

技术奖三等奖（3）

张宝宝、王旸旸

IP-to-AS映射修正粒度的系统分析
获得精确的IP-to-AS映射表，对于网络管理人员诊断网络故障和对于网络研究人员发现AS级网络拓扑有着重要的意义。一种获得IP-to-AS映射表的方法是基于traceroute路径和BGP 的AS路径是一致的假设，通过最大化匹配traceroute和BGP路径对的数量，来修正从路由表里提取的初始的IP-to-AS映射表。关于修正这个初始的IP-to-AS映射表，有两种粒度的修正方法，一种是/24前缀粒度的修正方法[1]，另一种是IP地址粒度的修正方法[2]。IP地址粒度的修正方法相比于前缀粒度的修正方法，可以大大提高路径对的匹配度。但是前缀粒度的方法和IP地址粒度的方法各有优缺点，本文提出了一种系统化的基于分类树的分析方法，可以系统、全面和定量的分析前缀粒度方法和IP地址粒度方法各自的优缺点。
详细 >>

蒋运韫、杨弋、肖 天

使用调试寄存器进行Linux内核数据竞争检测
并发程序中的数据竞争问题很难被检测和修复.以往的研究大多针对用户层的数据竞争检测并在此问题上取得了重大的进展,但在操作系统内核层面的数据竞争问题却几乎没有涉及.内核代码使用的同步机制远比用户层应用程序中复杂,如不同种类的锁,软硬件中断,大量的信号量原语以及各种底层的共享资源等.这些差别使得原有的用户层检测方法很难被应用到内核环境中.本文给出一个可有效检测Linux操作系统内核数据竞争问题的工具,基于当前通用处理器中现有的硬件结构调试寄存器,使用动态检测方法在内核程序运行过程中捕获数据竞争.初步的实验结果显示,本工具可有效地检测到内核中的数据竞争实例.
详细 >>

单来祥

基于按需即时去扩展化的LTL公式到Büchi自动机直接转换算法研究
在显式状态模型检测技术领域，现实系统通常被表达成线性时序逻辑(LTL)公式，并被转换成Büchi自动机(BA)。为了提高转换的效率，当前很多转换工具使用了中间自动机，如扩展的Büchi自动机(GBA)。去扩展化就是将GBA转换成BA的过程。本文提出并实现了LTL公式到BA的直接转换算法。本文中首次提出使用一个新的标签---接受度(Acceptance Degree，)用于记录转换过程中状态和变迁上已经满足的接受条件。是给定的LTL公式中子公式的集合。根据，本文提出一种不同于经典去扩展化算法的方法---按需即时的去扩展化(On-the-fly De-generalization，)算法。算法在展开LTL公式的过程中根据需要执行，它不同于完全展开LTL公式后，再进行去扩展化的经典方法。利用算法，我们实现了LTL 公式到Büchi自动机的直接转换，不需要使用中间自动机保存转换过程中临时结果。通过使用五组常用的LTL公式和四组随机生成的LTL公式测试已有的转换工具和本文提出转换工具，实验结果显示本文提出的直接转换方法避免了传统转换算法中的多重转换步骤，降低了计算复杂度，所需的转换时间更短。
详细 >>