Download Research Tools
A special report in the April 19, 2014, issue of The Economist predicted that 70 percent of China’s population—some 1 billion people—will live in cities by 2030. While China’s urban growth offers a higher standard of living to many citizens, it also creates serious problems.
Among these urban problems, noise pollution ranks among the most pervasive, as factories, construction projects and vehicles produce a cacophony of unwholesome sounds, with deleterious effects on the mental and physical well-being of city dwellers. Unfortunately, existing tools fail to track simultaneous sources of noise pollution accurately in real time, leaving researchers with an incomplete picture of the problem and how to address it. Clearly, researchers need a better way of tracking urban noise.
Noises permeate urban areas
Creating a noise map with smartphones
With funding from Microsoft Research Asia, investigators in the Department of Computer Science and Engineering at Shanghai Jiao Tong University, led by Professor Yanmin Zhu, are developing NoiseSense, a service that will map urban noises by using crowdsourced noise measurements from smartphone users. They envision a noise-mapping service that will allow anyone to query the noise level in any urban area in the world. More importantly, NoiseSense could give authorities the information needed to devise and implement effective noise-abatement strategies.
Sample noise map of Shanghai based on NoiseSense data
NoiseSense user interface on a Windows Phone
System design of NoiseSense
Accelerating urban informatics with Microsoft Azure
A future in which smartphone users willingly measure noise levels and a super computer system stands ready to crunch the resulting avalanche of data may seem idealistic, but it is exactly what Zhu and his team are striving to achieve. Having spent six months at Microsoft Research Asia as the recipient of a Young Faculty Program award, Zhu was familiar with the company’s research into the burgeoning field of urban informatics. Thus he was well positioned to apply for one of the grants offered by the Microsoft Azure for Research Award program—and delighted when his team’s proposal was one of only 25 Asian submissions (out of 60) to be funded. Taking advantage of the grant of free cloud-computing service on Microsoft Azure, Zhu’s team cleared the hurdle of managing large-scale noise data.
“I have really enjoyed our collaborations with Microsoft Research Asia in the past two years,” says Zhu. “I benefit a lot from many Microsoft academic programs including, but not limited to, the Accelerating urban informatics with Microsoft Azure program, Microsoft Azure for Research program and Microsoft Research AsiaYoung Faculty program. Furthermore, a couple of my graduate students have been well trained through this noise sensing project and one of my students received a Microsoft Research Asia Fellowship Finalist award last year. I look forward to more in-depth collaborations with Microsoft in the future.”
The urban computing initiative
Zhu’s team has made significant progress with the help of Microsoft Azure and the support of Microsoft Research Asia. They have developed a system prototype for a real-time, fine-grained noise-mapping service on Microsoft Azure, and they have created noise-measuring smartphone apps for both Windows Phone and Android operating systems.
Yu Zheng, a lead researcher at Microsoft Research, has worked closely with Zhu on the noise-mapping project, sharing his experience and expertise in the field of urban informatics. In fact, Zheng piloted Microsoft Research’s Urban Computing project, which has promoted computing applications designed to improve many aspects of city life, including urban transportation, air quality and energy consumption, as well as noise pollution.
Noise mapping and other urban computing research programs represent just a small percentage of the numerous ways that big data and computing can contribute to a better life for city dwellers. Researchers are only in the early days of exploiting the power and potential of urban computing—and we’re excited to be part of this momentous adventure.
—Kangping Liu, Senior Research Program Manager, Microsoft Research
As described during a press conference on April 23, Yonsei University and Microsoft Research have joined hands to develop the first computational thinking (CT) curriculum in Korea. Designed to nurture innovation and problem-solving, the curriculum aims to prepare talented students to employ computational thinking for the betterment of society. Students at Yonsei’s International Campus at Songdo will be the first beneficiaries of the CT classes, which will begin in the 2015–2016 school year.
Speakers at the press conference included Kap-Young Jeong, president of Yonsei University (top), and Miran Lee of Microsoft Research, the author of this blog (bottom).
Jeannette Wing, corporate vice president at Microsoft Research, coined the term "Computational Thinking" to describe the thought process involved in solving complex, real-world problems by using computer science theories, technologies, and other digital tools. She ranks among CT’s leading theorists and strongest advocates.
The hallmark of computational thinking is the ability to decompose complex, open-ended problems and apply generalized solutions. To give a very simple example, CT would find an optimal solution for making a mocha latte at a café by first analyzing the many variables of this procedure: how to get an empty cup, how to fill it with espresso, how to add steamed milk and flavored syrup, how to fit the cup with a lid, and finally, how to hand it to the customer. In the process of analyzing these discrete variables, computational thinking would reveal the underlying general problem and its overarching solution: how to accomplish all of these steps without disturbing other café workers.
"Korean students are good at resolving specific, given questions, but they lack ability to analyze and define exactly what the general problem is,” said Jung-Eun Nah, a professor of computer science at Yonsei. “We will concentrate on teaching students to identify problems in their daily lives and devise solutions step by step."
At the launch event, Kyung-Ho Lee, vice president of Yonsei University, stressed that the university understands the value of such problem-solving skills in this digital era, and that CT is the best way to instill these capabilities in students, empowering them to solve challenges across all academic areas and in every aspect of real life.
Speaking on behalf of Microsoft Research, I emphasized the inclusive nature of the new CT curriculum, noting that Yonsei is the first university in Korea to develop a CT curriculum for all its students.
Yonsei University plans to complete the CT curriculum development by July 2015 and to offer a limited number of CT courses shortly thereafter. The CT curriculum will expand to include all new students entering the Songdo campus in 2016. Science and engineering students will be required to take advanced CT classes as part of their major, while liberal arts students will take introductory CT courses as part of their basic education requirements. Eventually, Yonsei plans to implement the CT curriculum at its Shinchon Campus as well, where it will be taught in combination with various majors.
"CT education is expected to help the school greatly in nurturing students' creative thinking and problem-solving skills, and we will take full advantage of our excellent education-research infrastructure in the Songdo International Campus," said Kap-Young Jeong, president of Yonsei University. "We will continue,” he added, “to work closely with Microsoft to foster creative talents who can lead the digital society of the future."
—Miran Lee, Principal Research Program Manager, Microsoft Research
On Monday, June 15, Microsoft Research’s Z3 theorem prover received the 2015 ACM SIGPLAN Programming Languages Software Award. This prestigious award honors an institution or individuals for “developing a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both.” The announcement took place during PLDI 2015, the annual ACM SIGPLAN conference on Programming Language Design and Implementation.
Z3’s lead developers—Nikolaj Bjorner, Leonardo de Moura and Christoph Wintersteiger, all of Microsoft Research—were cited for creating a highly efficient theorem prover and tool in the SMT (Satisfiability Modulo Theories) class.
Derek Dreyer, Chair of the Awards Committee, presents the award to Christoph Wintersteiger, Leonardo de Moura and Nikolai Bjorner
Z3 is a state-of-the art theorem prover that integrates specialized solvers for domains that are of relevance for program analysis, testing and verification. Z3 is a compelling integral component of such tools because these tools rely on reasoning about program states and transformations between states.
Many years in the making, Z3 now supports all major platforms (Windows, OSX, Linux and FreeBSD). Since the code was released in October 2012, Z3 has been downloaded more than 20,000 times. Users can also call Z3 procedurally by using a variety of APIs available in C, C++, Java, .Net, OCaml and Python. Z3 became open source under an MIT license in March 2015.
With this release, Z3 has been adopted by an appreciative user community in a variety of tools for a wide range of uses, including general problem-solving, scheduling, optimization and software analysis. Being open source has definitely accelerated the development of the power of the system, in particular by accumulating contributions from the academic world, including theorists, tool-builders and users, for the benefit of all. Examples of tools in static analysis, verification and inference are Verifast, ScalaZ3, Why3, MetiTarski, SBV and ESC/Java2
In the academic world, Z3 has spawned more than 30 technical publications and more than 2,200 citations. It also provides an important tool for introducing students to SMT and theorem proving.
So congratulations to the Z3 team for this well-deserved recognition. You can try Z3 out in your own browser at Rise4Fun and find out more on the project website.
—Judith Bishop, Director of Computer Science, Microsoft Research, Tom Ball, Research Manager and Principal Researcher, Microsoft Research, and Ben Zorn, Research Manager and Principal Researcher, Microsoft Research