时间: 2014年7月2日-31日

参加人数: 27人

课程:

• 课程安排: Cornell Summer Program
• 程序语言（Programming Language）by David Gries and Michael Clarkson
• 专业实践（Specialty Practice） by John Hopcroft

学术报告:

2:00pm, July 2: Majority is not Enough: Bitcoin Mining is Vulnerable by EMİN GÜN SİRER

• The Bitcoin cryptocurrency records its transactions in a public log called the blockchain. Its security rests critically on the distributed protocol that maintains the blockchain, run by participants called miners. Conventional wisdom asserts that the protocol is incentive-compatible and secure against colluding minority groups, i.e., it incentivizes miners to follow the protocol as prescribed.
• We show that the Bitcoin protocol is not incentive-compatible. We present an attack with which colluding miners obtain a revenue larger than their fair share. This attack can have significant consequences for Bitcoin: Rational miners will prefer to join the selfish miners, and the colluding group will increase in size until it becomes a majority. At this point, the Bitcoin system ceases to be a decentralized currency.
• Selfish mining is feasible for any group size of colluding miners. We propose a practical modification to the Bitcoin protocol that protects against selfish mining pools that command less than 1/4 of the resources. This threshold is lower than the wrongly assumed 1/2 bound, but better than the current reality where a group of any size can compromise the system.

9:00am, July 3: NetKAT: Semantic Foundations for Networks by Dexter Kozen

• Recent years have seen growing interest in high-level languages for programming networks. But the design of these languages has been largely ad hoc, driven more by the needs of applications and the capabilities of network hardware than by foundational principles. The lack of a semantic foundation has left language designers with little guidance in determining how to incorporate new features, and programmers without a means to reason precisely about their code.
• This paper presents NetKAT, a new network programming lan- guage that is based on a solid mathematical foundation and comes equipped with a sound and complete equational theory. We describe the design of NetKAT, including primitives for filtering, modifying, and transmitting packets; union and sequential composition oper- ators; and a Kleene star operator that iterates programs. We show that NetKAT is an instance of a canonical and well-studied mathe- matical structure called a Kleene algebra with tests (KAT) and prove that its equational theory is sound and complete with respect to its denotational semantics. Finally, we present practical applications of the equational theory including syntactic techniques for checking reachability, proving non-interference properties that ensure isola- tion between programs, and establishing the correctness of compi- lation algorithms.

4:00pm, July 10: The Role of Type Theory in the Use of Proof Assistants for Programming, Software Engineering, and Computing Theory by Bob Constable

• An interesting trend in computer science research in Europe and the United States is the increasing use of proof assistants. These are computing systems that help people solve mathematical problems, including writing formal proofs that programs meet their specifications.
• These proof assistants are also being used by mathematicians and theoretical computer scientists to formally prove difficult theorems.
• The most widely used proof assistants are Coq and HOL. The Coq proof assistant is closely related to the Nuprl proof assistant built at Cornell and supported here. All of these proof assistants are based on type theory as their mathematical language, rather than set theory.
• This lecture will explain elements of type theory and show how it is used to specify programs and prove that programs meet these specifications. We will also illustrate how type theory is used in mathematics.

4:00pm, July 14 Juris Hartmanis

• Hartmanis教授回顾了他从事计算机科学的原因和他的早期的科研生涯。Hartmanis教授是拉脱维亚人，在第二次世界大战结束之后，他正好高中毕业，全家搬去了德国，Hartmanis教授在Marburg大学完成了本科学业，专业是物理。毕业之后，Hartmanis教授搬去了美国，在Kansas City大学完成了master学业，专业是应用数学，之后又在加州理工学院获得了数学博士学位。
• 1955年Hartmanis教授博士毕业之后，在Cornell大学获得了教职，两年后又去了Ohio State大学。1958年，Hartmanis教授加入了通用电气研究实验室，在通用电气期间，他对计算复杂性理论产生了兴趣并且对这一领域做出了一些贡献。1965年，他回到Cornell大学担任教授，Cornell大学此时正在筹办计算机科学系，在此之前，Cornell大学关于计算理论的研究都是在数学系完成的，他们认为此时成立计算机科学系的时机已经成熟，应该把和计算机科学相关的研究和教学分离出去。Hartmanis教授担任了计算机科学系的第一任系主任。在Hartmanis教授担任系主任期间，他招来了一批优秀的计算机科学家来Cornell大学任教和研究，包括John Hopcroft、David Gries、Robert Constable。他们对Cornell大学的计算机系都做出了很大贡献，并且一直在Cornell工作至今。

2:00pm, July 15 - 17 Ken Birman

• He introduced smart power grid. Smart power grid combines system and machine learning together. Ken aims at building a system for the smart grid so that it can work as an iPad. We can add sensors everywhere to monitor the global state of the grid. Then software for better arranging the power can be added to the system like apps to the iPad.
• Some puzzles in the system world such as two generals and muddy children.
• Introduction to the smart meter at home. He talked about what applications these meters can have and how they can improve our life.

4:00pm, July 15 Doug James

Normally, the sound in the cartoon are wrong. To produce the sound, people normally just record the sound that they think the true sound is like to be. So Doug James focuses on how to generate the sound better. He presented a lot of projects he has done, like how to generate the sound of water, fire and how to speed them up, how to generate the sound of broken glass which involves plenty of objects, how to model the sound of clothing and so on.

4:00pm, July 16 Eva Tardos

从博弈论发展至今，最有影响力的结果当属纳什均衡，但是纳什均衡仍有很多缺陷，如计算复杂度高、PoA等。Eva Tardos提出了一种新的基于学习的标准代替纳什均衡，在重复博弈中设置regret函数，参与者在regret函数达到threshold时根据best response改变策略，可以证明在所有参与者都采取该策略的情况下social welfare不会比采取纳什均衡的情况差，并且在很多经典案例中都可以得到更好的结果。

11:00am, July 23 Thorsten

Say we have two ranking function for some search engine. When we do experiments to test which function is better, we usually randomly divide people into 2 groups and use some features like #of clicks on the top 1 item to judge. However, this method has two problems. 1. Thorsten’s group has done some experiments and showed that none of the previous metrics truly shows whether a rank function is better than the other. 2. The previous method is silly because it’s just like divide people into 2 groups and ask one group how much they like Coca Cola and ask the other group how much they like Pepsi. What we should do is to ask each person which they like more, Coca Cola or Pepsi. Therefore, they interleaved the results generated by the two functions and showed the combined results to the users. Then they measure something like how many clicks each function receives to compare them. Their experiments show that this method truly shows which function is better. Moreover, based on this interleaving result method, they derived an algorithm to quickly find the best rank function by pairwise comparison only.

11:00am, July 25 Kavita Bala

She works on graphics and introduced 4 main projects. The first two are in rendering. Previously, people need to develop a new model whenever they encounter a new material. Her group developed a method that can systematically handle most kinds of clothing including velvet, silk, wool and so on. It first uses CT scan to obtain the 3d model of the material, then it adjusts some parameters to let the material look like the true material. Finally, it obtains the final rendering result. Since the rendering involves too many details, it’s very slow. So they further proposed a new method to speed it up. The last two projects is on building a database for materials. We now have large datasets for images but not materials. To enhance research on material, they developed the first large-scale database for materials that can extracts the surface of a wood floor, for example, and can obtain its color information, reflectance information, etc. In the fourth project, they build a database which provides pairwise comparison between the true color of the material (disregard of the shading).

2:00pm, July 28 Jon Kleinberg

In social network, people often share images, share blogs and share everything. Some information is widely spread while others are not. When we closely observe the graph of how the message is shared, we can find some structure in the graph that leads to this difference. Therefore, he design a method to predict how well some information will be spread (cascade) given the “share graph” so far. Secondly, we often use the metric - how many friends two people share - to measure how closely related the two people are. However, it’s not often the case. When two people are coworkers, even if they are not good friends, they share a lot of coworkers as friends. So he introduced another metric to measure the closeness of two people. And it showed good performance in predicting a spouse.

11:00am, July 29 Charles F. Van Loan

We have done much study on the matrix. However, nowadays matrix is not enough and people often have to deal with tensors (A tensor is just a multidimensional array and a matrix is a 2-dim tensor). He introduced how people can analyze a tensor and how symmetry in multi-dimension can lead to interesting properties when we unfold a 4-d tensor into a 2-d matrix.

以上学术报告概要，感谢罗璇、杨宽、陈志鹏等同学整理提供

我的康奈尔科研之旅(2011级ACM计算机科学班)

多彩生活: