Download Research Tools
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
Mosquitoes. They can ruin your backyard barbeque and leave you covered with itchy welts. Or, their bites may also transmit dangerous pathogens. The World Health Organization estimates that mosquito-borne diseases kill more than 1 million people annually. In fact, mosquitoes do more than just transmit pathogens. Their ability to locate and sample the blood of many species of animals means they can be used to monitor pathogens carried by animals in the wild. In a sense, we can view mosquitoes as naturally occurring devices that sample the animal population. This is important, because many diseases—such as Ebola, SARS and MERS—reside in animals and emerge into the human population through complex interactions with animals.
Disease emergence is difficult to predict, and can be catastrophic and extraordinarily expensive even if the disease does not become an epidemic. Usually, health officials only learn about an outbreak once people are already getting sick. And by then, it’s too late.
Project Premonition was created with the hope of detecting diseases prior to outbreaks. And unique to this emerging infectious disease (EID) surveillance system is the use of the mosquito-as-a-device to obtain samples of pathogens from well-hidden animal populations. The hope is that Premonition addresses the drawbacks of existing systems.
Through Project Premonition, we have not only brought together experts within Microsoft Research from hardware prototyping, software development for safe and autonomous drone deployment and machine learning, but experts at universities in public health, genetics, computer science, systems integration, mosquito-trap design and drone aeronautics—all with a goal of learning how to detect diseases before they erupt into epidemics.
This cross-disciplinary research will be conducted between world-class researchers from the following universities:
Of course, trapping mosquitoes and testing them for the presence of infectious agents isn’t anything new, but up until now it has been a slow, labor-intensive process specialized for a few known pathogens. Large-scale autonomous collection and broad-spectrum analysis had not been considered. So, our first step was accomplished a couple of months ago when we conducted a feasibility study in Grenada, a Caribbean island that features a variety of ecosystems and an abundance of mosquitoes. It was the perfect location, as we also received generous support from St. George's University faculty, who were able to provide essential knowledge of the area and local mosquito populations in addition to laboratory facilities.
We envision a worldwide system for collection and genomic analysis of mosquitoes, capable of detecting potential pathogens and their geographic spread, before they cause disease in the human population. Such a global system will require scalable, robust and safe autonomous systems and tremendous computational power—and the kind of industry-academia cooperation that is vital to Microsoft Research efforts like Project Premonition.
You can also learn more about the project on the Next at Microsoft Blog and Project Premonition project page.
—Ethan Jackson, Researcher, Microsoft Research