2011年“二十一世纪的计算”学术研讨会

Emmanuel Candes is a Professor of Mathematics, a Professor of Statistics, a Professor of Electrical Engineering (by courtesy) and a member of the Institute of Computational and Mathematical Engineering at Stanford University. He is also the Ronald and Maxine Linde Professor of Applied and Computational Mathematics at the California Institute of Technology (on leave). He received the Ph.D. degree in statistics from Stanford University in 1998. His research interests are in computational harmonic analysis and multiscale analysis, mathematical optimization, statistical estimation and detection with applications to the imaging sciences, signal processing, scientific computing, and inverse problems.

Professor Candes received numerous awards, most notably the 2006 Alan T. Waterman Medal, which is the highest honor bestowed by the National Science Foundation and which recognizes the achievements of scientists who are no older than 35, or not more than seven years beyond their doctorate. Other awards include the 2005 James H. Wilkinson Prize in Numerical Analysis and Scientific Computing awarded by the Society of Industrial and Applied Mathematics (SIAM), the 2008 Information Theory Society Paper Award, the 2010 George Polya Prize awarded by SIAM, and the 2011 Collatz Prize awarded by the International Council for Industrial and Applied Mathematics(ICIAM). He has given over 40 plenary lectures at major international conferences.

Presentation Title： Compressive Sensing

Abstract：
Compressive sensing is a new sampling/data acquisition theory based on the discovery that one can exploit sparsity or compressibility when acquiring signals of general interest, and that one can design nonadaptive sampling techniques that condense the information in a compressible signal into a small amount of data. Interestingly, this may be changing the way engineers think about signal acquisition in areas ranging from analog-to-digital conversion, digital optics, magnetic resonance imaging, and seismics. This talk will introduce fundamental conceptual ideas underlying this new sampling or sensing theory. There are already many ongoing efforts to build a new generation of sensing devices based on compressive sensing, and we will address remarkable recent progress in this area as well.

Edmund M. Clarke received a B.A. degree in mathematics from the University of Virginia, Charlottesville, VA, in 1967, an M.A. degree in mathematics from Duke University, Durham NC, in 1968, and a Ph.D. degree in Computer Science from Cornell University, Ithaca NY, in 1976. After receiving his Ph.D., he taught in the Department of Computer Science, Duke University, for two years. In 1978 he moved to Harvard University, Cambridge, MA where he was an Assistant Professor of Computer Science in the Division of Applied Sciences. He left Harvard in 1982 to join the faculty in the Computer Science Department at Carnegie-Mellon University, Pittsburgh, PA. He was appointed Full Professor in 1989. In 1995 he became the first recipient of the FORE Systems Professorship, an endowed chair in the School of Computer Science. He was named a University Professor in 2008.

Dr. Clarke’s interests include software and hardware verification and automatic theorem proving. In his Ph.D. thesis he proved that certain programming language control structures did not have good Hoare style proof systems. In 1981 he and his Ph.D. student Allen Emerson first proposed the use of Model Checking as a verification technique for finite state concurrent systems. His research group pioneered the use of Model Checking for hardware verification. Symbolic Model Checking using BDDs was also developed by his group. This important technique was the subject of Kenneth McMillan’s Ph.D. thesis, which received an ACM Doctoral Dissertation Award. In addition, his resarch group developed the first parallel resolution theorem prover (Parthenon) and the first theorem prover to be based on a symbolic computation system (Analytica).

Dr. Clarke has served on the editorial boards of Distributed Computing, Logic and Computation, and IEEE Transactions in Software Engineering. He is the former editor-in-chief of Formal Methods in Systems Design. He is on the organizing committee of Logic in Computer Science (LICS) and on the steering committee of  Computer-Aided Verification (CAV). He received a Technical Excellence Award with Randy Bryant and Ken McMillan from the Semiconductor Research Corporation in 1995 for his work on formal verification techniques. He was a co-winner with Randy Bryant, Allen Emerson, and Kenneth McMillan of the ACM Kanellakis Award in 1998 for the development of Symbolic Model Checking.  In 1999 he received an Allen Newell Award for Excellence in Research from the Carnegie Mellon Computer Science Department.  In 2004 he received the IEEE Harry H. Goode Memorial Award for significant and pioneering contributions to formal verification of hardware and software systems, and for the profound impact these contributions have had on the electronics industry.  He was elected to the National Academy of Engineering in 2005 for contributions to the formal verification of hardware and software correctness.  He was a recipient with Allen Emerson and Joseph Sifakis of the 2007 ACM Turing Award for his role in developing Model Checking into a highly effective verification technology, widely adopted in the hardware and software industries.  In 2008 he received the CADE Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of his role in the invention of Model Checking and his sustained leadership in the area for more than two decades. In 2011 he was elected to the American Academy of Arts & Sciences which includes distinguished leaders in the sciences, social sciences, the humanities, the arts, as well as business and public affairs. Dr. Clarke is a Fellow of the ACM and the IEEE, and a member of Sigma Xi and Phi Beta Kappa.

Presentation Title： Model Checking and the Curse of Dimensionality

Abstract：
The term “Curse of Dimensionality” was coined by the famous mathematician, Richard Bellman.  He used the term to describe the exponential increase in volume associated with adding extra dimensions to an object in space.  One implication of the Curse of Dimensionality is that methods for numerical solution of various optimization problems require vastly more computer time when the number of state variables involved increases.  A similar phenomenon occurs in temporal logic model checking.  Model checking is an automatic verification technique for concurrent systems that are finite state or have finite state abstractions.  It has been used successfully to verify computer hardware and is beginning to be used to verify computer software as well. As the number of processes in the system increases, the number of global system states grows exponentially.  This is called the state explosion problem. Much of the research in model checking over the past 30 years has involved developing techniques for dealing with this problem.  In this talk I will describe some recent approaches to the state explosion problem using compositional reasoning, abstract interpretation, and statistical sampling techniques.  I will give examples about how these techniques can be used to make model checking feasible for computer software and to understand molecular processes in systems biology.

Joseph Halpern received a B.Sc. in mathematics from the University of Toronto in 1975 and a Ph.D. in mathematics from Harvard in 1981.  In between, he spent two years as the head of the Mathematics Department at Bawku Secondary School, in Ghana. After a year as a visiting scientist at MIT, he joined the IBM Almaden Research Center in 1982, where he remained until 1996, also serving as a consulting professor at Stanford.  In 1996, he joined the CS Department at Cornell, and is now department chair.

Halpern’s major research interests are in reasoning about knowledge and uncertainty, security, distributed computation, decision theory, and game theory.  Together with his former student, Yoram Moses, he pioneered the approach of applying reasoning about knowledge to analyzing distributed protocols and multi-agent systems.  He has coauthored 6 patents, two books (“Reasoning About Knowledge” and “Reasoning about Uncertainty”), and over 300 technical publications.

Halpern is a Fellow of the AAAI, the ACM, and the AAAS.  Among other awards, he received the ACM SIGART Autonomous Agents Research Award n 2011, the Dijkstra Prize in 2009, the ACM/AAAI Newell Award in 2008, the Godel Prize in 1997, was a Guggenheim Fellow in 2001-02, and a Fulbright Fellow in 2001-02 and 2009-10. Two of his papers have won best-paper prizes at IJCAI (1985 and 1991), and another won one at the Knowledge Representation and Reasoning Conference (2006). He was editor-in-chief of the Journal of the ACM (1997-2003) and has been program chair of a number of conferences, including the Symposium on Theory in Computing (STOC), Logic in Computer Science (LICS), Uncertainty in AI (UAI), Principles of Distributed  Computing (PODC), and Theoretical Aspects of Rationality and Knowledge (TARK).

Presentation Title： Solution Concepts for the 21st Century

Abstract：
Nash equilibrium is the most commonly-used notion of equilibrium in game theory.  However, it suffers from numerous problems.  Some are well known in the game theory community; for example, the Nash equilibrium of repeated prisoner’s dilemma is neither normatively nor descriptively reasonable. However, new problems arise when considering Nash equilibrium from a computer science perspective: for example, Nash equilibrium is not robust (it does not tolerate “faulty” or “unexpected” behavior), it does not deal with coalitions, it does not take computation cost into account, and it does not deal with cases where players are not aware of all aspects of the game.  In this talk, I discuss solution concepts that try to address these shortcomings of Nash equilibrium.  This talk represents joint work with various collaborators, including Ittai Abraham, Danny Dolev, Rica Gonen, Rafael Pass, and Leandro Rego.  No background in game theory will be presumed.

Dr. Hsiao-Wuen Hon is the Managing Director of Microsoft Research Asia, located in Beijing, China. Founded in 1998, Microsoft Research Asia has since become one of the best research centers in the world that MIT Technology Review called “the hottest computer science research lab in the world.” Dr. Hon oversees the lab’s research activities and collaborations with academia in Asia Pacific.

An IEEE fellow and a Distinguished Scientist of Microsoft, Dr. Hon is an internationally recognized expert in speech technology. He serves on the editorial board of the international journal of the Communication of the ACM. Dr. Hon has published more than 100 technical papers in international journals and at conferences. He co-authored a book, Spoken Language Processing, which is a graduate-level textbook and reference book in the area of speech technology in many universities all over the world. Dr. Hon holds three dozens of patents in several technical areas.

Dr. Hon has been with Microsoft since 1995. He joined Microsoft Research Asia in 2004 as a Deputy Managing Director, responsible for research in Internet search, speech & natural language, system, wireless and networking. In addition, he founded and managed search technology center (STC) from 2005 to 2007, the Microsoft internet Search product (Bing) development in Asia Pacific.

Prior to joining Microsoft Research Asia, Dr. Hon was the founding member and architect in Natural Interactive Services Division at Microsoft Corporation. Besides overseeing all architectural and technical aspects of the award winning Microsoft® Speech Server product (Frost & Sullivan’s 2005 Enterprise Infrastructure Product of the Year Award, Speech Technology Magazine’s 2004 Most Innovative Solutions Awards and VSLive! 2004 Editors Choice Award.), Natural User Interface Platform and Microsoft Assistance Platform, he is also responsible for managing and delivering statistical learning technologies and advanced search. Dr. Hon joined Microsoft Research as a senior researcher at 1995 and has been a key contributor of Microsoft’s SAPI and speech engine technologies. He previously worked at Apple Computer, where he led research and development for Apple’s’ Chinese Dictation Kit.

Dr. Hon received Ph.D in Computer Science from Carnegie Mellon University and B.S. in Electrical Engineering from National Taiwan University.

As senior vice president, Rick F. Rashid oversees worldwide operations for Microsoft Research, an organization encompassing more than 850 researchers across six labs worldwide. Under Rashid’s leadership, Microsoft Research conducts both basic and applied research across disciplines that include algorithms and theory; human-computer interaction; machine learning; multimedia and graphics; search; security; social computing; and systems, architecture, mobility and networking. His team collaborates with the world’s foremost researchers in academia, industry and government on initiatives to advance the state-of-the-art of computing and to help ensure the future of Microsoft’s products.

After joining Microsoft in September 1991, Rashid served as director and vice president of the Microsoft Research division and was promoted to his current role in 2000. In his earlier roles, Rashid led research efforts on operating systems, networking and multiprocessors, and authored patents in such areas as data compression, networking and operating systems. He managed projects that catalyzed the development of Microsoft’s interactive TV system and also directed Microsoft’s first e-commerce group. Rashid was the driving force behind the creation of the team that later developed into Microsoft’s Digital Media Division.

Before joining Microsoft, Rashid was professor of computer science at Carnegie Mellon University (CMU). As a faculty member, he directed the design and implementation of several influential network operating systems and published extensively about computer vision, operating systems, network protocols and communications security. During his tenure, Rashid developed the Mach multiprocessor operating system, which has been influential in the design of modern operating systems and remains at the core of several commercial systems.

Rashid’s research interests have focused on artificial intelligence, operating systems, networking and multiprocessors. He has participated in the design and implementation of the University of Rochester’s Rochester Intelligent Gateway operating system, the Rochester Virtual Terminal Management System, the CMU Distributed Sensor Network Testbed, and CMU’s SPICE distributed personal computing environment. He also co-developed of one of the earliest networked computer games, “Alto Trek,” during the mid-1970s.

Rashid was inducted into the National Academy of Engineering in 2003 and presented with the Institute of Electrical and Electronics Engineers Emanuel R. Piore Award and the SIGOPS Hall of Fame Award in 2008. He was also inducted into the American Academy of Arts & Sciences in 2008. In addition, Rashid is a member of the National Science Foundation Computer Directorate Advisory Committee and a past member of the Defense Advanced Research Projects Agency UNIX Steering Committee and the Computer Science Network Executive Committee. He is also a former chairman of the Association for Computing Machinery Software System Awards Committee.

Rashid received master of science (1977) and doctoral (1980) degrees in computer science from the University of Rochester. He graduated with honors in mathematics and comparative literature from Stanford University in 1974.

Andrew Chi-Chih Yao is a professor and dean of the Interdisciplinary Information Sciences (IIIS) at Tsinghua University in Beijing. His research interests include analysis of algorithms, computational complexity, cryptography, and quantum computing. From 1975 to 1986, Professor Yao was a faculty member at MIT, Stanford University, and the University of California, Berkeley He was the William and Edna Macaleer professor of engineering and applied science at Princeton University from 1986 to 2004, at which point, he left Princeton to become a professor of computer science at Tsinghua University in Beijing. He is also a Distinguished Professor-at-Large at the Chinese University of Hong Kong. Professor Yao’s research interest include the theory of computation and its application in cryptography and quantum computing, and has made research contributions in three ways: creation of important subfields for theoretical computer science; helping to develop the foundations of modern cryptography; and resolving open problems and establishing new paradigms in circuit complexity, computational geometry, data structures, and quantum computing. He was recipient of the A M Turing Award in 2000 for his contributions to the theory of computation, including communication complexity, pseudorandom number generation, and quantum communication. His numerous other honors and awards include the George Polya Prize, the Donald E Knuth Prize, and several honorary degrees from the Chinese University of Hong Kong, the City University of Hong Kong, the Hong Kong University of Science and Technology, and the University of Waterloo. Professor Yao is a member of the US National Academy of Sciences, the American Academy of Arts and Sciences, and the Chinese Academy of Sciences. He holds a PhD in physics from Harvard University, a PhD in computer science from the University of Illinois, and a BS in Physics from National Taiwan University.

Presentation Title： Quantum Computing: A Great Science in the Making

Abstract：
In recent years, the scientific world has seen much excitement over the development of quantum computing, and the ever increasing possibility of building real quantum computers. What’s the advantage of quantum computing? What are the secrets in the atoms that could potentially unleash such enormous power, to be used for computing and information processing? In this talk, we will take a look at quantum computing, and make the case that we are witnessing a great science in the making.