Download Research Tools
Building verifiably reliable and trustworthy software is one of the ultimate objectives of software engineering. With this goal in mind, academics, scientists, and researchers gathered in Shanghai, China, for the second Verified Software Workshop and Summer School. The event, which took place from August 23 to 31, 2012, attracted approximately 250 faculty and student attendees from more than 70 universities and research institutes and nearly a dozen countries across the Asia Pacific region and beyond.
World-class scientists and researchers—from Asia, Europe, and North America—provided the latest insights into verification theory, practice, and tools.
Co-sponsored by Microsoft Research Asia and East China Normal University, the event explored new directions and emerging opportunities in verified software research, with 21 keynote presentations by world-class scientists and researchers—from Asia, Europe, and North America—providing the latest insights into verification theory, practice, and tools. Especially notable among the prominent presenters were the workshop co-chairs: Professor Tony Hoare, the 1980 Turing Award winner and a principal researcher at Microsoft Research Cambridge, who gave the opening speech, titled, “Algebra Unifies Theories of Programming”; and Professor Jifeng He of East China Normal University and a member of the of the Chinese Academy of Sciences, who delivered a keynote on “A Clock-Based Framework for Modeling Hybrid Systems.”
The event began with a two-day workshop at East China Normal University that included inspiring lectures from technical and academic leaders. A broad and comprehensive workshop, it featured in-depth talks on such topics as detection of concurrency bugs, safe programming of asynchronous interaction, pervasive model checking, analysis and verification of multiple programs, automation of program verification, concurrent software verification, software analytics and its application, and modeling and verification of hybrid systems.
A five-day summer school of intense training followed the workshop. Students were treated to lectures focusing on the theoretical nature of concurrency and separation logic. One particular highlight was the hybrid systems session, which taught the KeYmaera logical analysis approach in a single day’s time. In addition, a step-by-step tool session provided attendees with valuable hands-on practice and an in-depth learning experience.
The event was popular with both students and presenters. Summing up the benefits of the event, one student said, “I acquired cutting-edge research and tools in [the] verification software field, and also had the opportunity to exchange my ideas with innovative peers and academic leads from across the world.”
Capturing the perspective of the experienced researcher, co-chair Tony Hoare praised the event and laid out his goals for such venues, saying, “We hope to expand the opportunities for industrial application of mature academic research, and to encourage the next generation of advanced researchers to continue the pursuit of deep and interesting questions in areas of the software industry.”
Professor Tony Hoare, the 1980 Turing Award winner and a principal researcher at Microsoft Research Cambridge, gave the opening speech, titled, “Algebra Unifies Theories of Programming."
Co-chair Jifeng He added, “We have achieved a lot in [the] verified software field with everyone’s great effort, but there is always more work to do. With this event, we hoped to not only inspire our young talent but also provide researchers and faculties worldwide with the advantage of exchanging ideas.”
Lolan Song, the senior director of Microsoft Research Asia, spoke of the company’s objectives in sponsoring such events, observing that “We hold this event in order to advance the state of the art in software and present a great opportunity for academics, researchers, and students in this area to share and exchange ideas. Also, we hope to identify and cultivate worldwide top talent in verified software areas and build up cadres of experienced users to support eventual use of the tools in the industry.” She also expressed the gratitude of Microsoft Research Asia for the assistance and participation of colleagues from Microsoft Research Cambridge, Microsoft Research Redmond, and Microsoft Research India.
—Kangping Liu, University Relations Manager, Microsoft Research Connections Asia
The 28th General Assembly of the International Astronomical Union (IAU) opened on August 20, 2012, at the China National Convention Center in Beijing, with WorldWide Telescope (WWT) prominently featured at the Microsoft Research exhibition.
Astronomy is one of the oldest and most inspirational areas of scientific discovery, and the two-week IAU General Assembly attracts thousands of attendees from around the world. Participants include researchers and educators not only in traditional astronomy and astrophysics disciplines but also those drawn from informatics, data science, and computer science. Even in this era of “big data,” astronomy remains one of the most data-intensive fields, which, in part, explains Microsoft Research’s long history of working with the astronomical community. The data- and information-intensive problems that arise as the astronomical community strives to create an all-sky survey (a survey of everything in the sky) and a virtual (online) observatory have stimulated many innovative software and engineering ideas at Microsoft Research and have fostered a rewarding collaboration with the astronomical community.
One of the most successful outcomes of this collaboration has been WWT, which enables a computer to function as a virtual telescope and more. The WWT software aggregates the best data and imagery from all the main space- and ground-based telescopes, providing incomparable views of the night sky. It also connects seamlessly to the information behind the imagery and allows users to layer their own data on top of the common sky and the Earth imagery. In so doing, WWT enables users to tell stories with data very easily.
Since its first release in early 2008, WWT has gained millions of users worldwide. For many astronomical professionals, especially educators, WWT has made a fundamental difference in their career. With an exponentially growing user community, we expect that WWT will continue to contribute to the advancement of computational astronomy research and science education. The growing value of WWT is summed up nicely by Harvard astronomer Alyssa Goodman and IAU President Robert Williams:
WWT was originally created as an educational tool, but it has rapidly become the very best example of the all-sky "Virtual Observatory" research astronomers have been working toward since the advent of the Internet. Today, WWT is the single richest source of astronomical imagery and links online, and it is loved by educators and researchers alike.
—Alyssa Goodman, Professor of Astronomy, Harvard University
I am immensely impressed with WWT as a teaching and outreach tool and what MR [Microsoft Research] has done to make it both appealing and practical. The IAU has recently commenced a large global program to use astronomy as a tool for education and technology development, and I believe that WWT should be a key element in that entire effort.
—Bob Williams, President, International Astronomical Union
Microsoft Research is proud to present the WorldWide Telescope at the 28th IAU General Assembly, in exhibition booth #46. Together with the WWT Ambassadors from Harvard University and academic collaborators from the National Astronomical Observatory of the Chinese Academy of Sciences and China Central Normal University, we are eager to engage with IAU2012 attendees and create more WWT success stories. In addition, we look forward to introducing visitors to other cutting-edge Microsoft technologies, including Layerscape, Microsoft Translator, and Kinect for Windows, and to advancing mutually beneficial collaborations between academia and Microsoft Research.
—Yan Xu, Senior Research Program Manager, Microsoft Research Connections, and Guobin Wu, Research Program Manager, Microsoft Research Asia
Korea’s Ministry of Knowledge Economy (MKE) recently announced that Microsoft Research Asia will once again be a key partner in the Information Technology Software Creative Research Program, which provides support to world-class researchers in that country. MKE plans to provide matching funds in the amount of five times the expenditures of Microsoft Research Asia (in other words, the ministry provides $5 for every $1 spent by Microsoft Research Asia) on collaborative research projects that are conducted by Korean academia.
“The collaboration with the Ministry of Knowledge Economy of Korea is a significant milestone in creating opportunities for universities to experience world-class research, discover potential talent, and accelerate innovation,” said Hsiao-Wuen Hon, Microsoft Research Asia managing director. “Microsoft Research Asia is committed to providing continuous support for Korean universities and government programs as a driving force in strengthening Korea’s IT competitiveness.”
Sixty Korean academics attended Korean Day on July 3, 2012,at Microsoft Research Asia in Beijing, China
As part of the program, Microsoft Research Asia offers internships to graduate-level students at its state-of-the-art facilities in Beijing, China. By providing the opportunity to participate in practical research, the internships help participating students improve their professional skills and increase their knowledge. During the first program, which started in September 2010, a total of 10 graduate students were awarded six-month internships at Microsoft Research Asia. Of those 10 students, five went on to participate in a 12-week summer internship program at Microsoft Research in Redmond, Washington.
“The internship program allowed me to experience and learn the research trends and techniques used at a global company,” said Hyunsun Seo, a 2011 Microsoft Research Asia fellowship winner and intern at Microsoft Research Asia and Redmond. “I used to presume research would be conducted in a manner similar to what I’ve done in school. Now, I have a clear picture about the similarities and differences. This insight will be hugely beneficial and will offer me a distinct edge as I plan my career path after graduation.”
The program has already produced a number of success stories. In its second year, 24 projects were selected out of 54 proposals for research related to topics such as hardware computing, human computing interaction, Internet graphics, Internet media, information retrieval and mining, media computing, wireless and networking, web retrieval and mining, web intelligence, web data management, system, speech recognition, theory, machine learning, and innovative engineering.
The students’ work was on display during the Korean Day event held on July 3 at the Microsoft Research Asia facilities in Beijing, China. Among those attending were 60 Korean academics, including faculty members and students.
—Miran Lee, Senior University Relations Manager, Microsoft Research Asia