Download Research Tools
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
How did you do in your high school linguistics courses? What? Your high school didn’t offer any linguistics classes? Well, you’re not alone; it’s difficult to find any secondary school in the world that formally teaches linguistics.
As a scientist, I find that unfortunate. It means that countless bright, inquisitive young people are never exposed to the scientific study of language, a subject that is both immensely important and intellectually satisfying. Analyzing the logical structure of language builds critical skills in computational thinking, a skillset that will be increasingly necessary in today’s digital world. Moreover, linguistics studies make students aware of the diversity of languages and cultures that enrich our world, opening their eyes to the fact that there are many ways to think about things. It also sensitizes them to the plight of dying languages, a process that is accelerating due to the prominence of a few major languages in modern media. Finally, in my country, India, as in many places, the way language is taught in school centers on grammar and literature; consequently, smart, analytically minded students are not exposed to the idea that language can be studied scientifically.
This is why my colleagues in the computational linguistics group at Microsoft Research India and I are staunch supporters of the International Linguistics Olympiad (IOL). This annual event, first held in 2002, is open only to high school students and thus offers a unique opportunity to introduce bright teenagers to the scientific and computational aspects of human language. Every participating country (around 30 in 2014) sends one or two teams of four students each. Participants needn’t have any theoretical background in linguistics. Instead, they solve some of the toughest linguistic problems through sheer analytical abilities and linguistic intuition, as shown in the video below.
Microsoft Research has a rich history in the area of language, having conducted fundamental research on natural language processing, speech-to-speech, and automated translation, so it was only natural that my colleagues and I at Microsoft Research India would see the value of the IOL—but it took a while. India first participated in the IOL in 2009; however, it was only in 2011 that a systematic national selection event, the Panini Linguistics Olympiad was introduced by the University of Mumbai. I came to know about the Olympiad from Prof. Dragomir Radev of the University of Michigan, who is the coach/team leader of the teams from the United States and an active organizer of the North American Computational Linguistics Olympiad (NACLO). He solicited help from Microsoft Research for sponsoring and promoting their Indian counterpart.
The Panini Linguistics Olympiad happens in two rounds: round 1, which involves a written test, takes place across several cities in India. The top 20 to 25 students are invited to round 2, which consists of a weeklong residential camp. During the camp, the students learn some basic linguistic concepts and various problem-solving techniques. Round 2 ends with a test that determines which students will represent India in one of the two teams we send to IOL this year.
2015 participants of the weeklong residential camp
After hearing from Prof. Radev, I scouted out the 2013 Panini Linguistics Olympiad camp. It was a fascinating experience; I enjoyed lecturing and interacting with a bunch of young talented students, as well as designing linguistic puzzles and problems for the selection test. The camp organizers—Prof. Avinash Pandey of Mumbai University and Zarana Sarda, program coordinator for the Panini Linguistics Olympiad—were very motivated; however, the program lacked financial and infrastructural support. There was very little awareness about the Olympiad, which was evident from the fact that only 26 students, mostly from Mumbai, had written the round 1 test that year. So, my colleagues Kalika Bali and A Kumaran and I decided to support the Panini Olympiad with support from Microsoft Research.
In 2014, Kalika and I contacted several linguists and computational linguists across the country and with their help, we set up five regional centers for the Olympiad. We also conducted a promotional workshop for students and teachers in Bangalore. Round 1 participation went up by a factor of 5! The weeklong round 2 camp was organized at Microsoft Research India and we also sponsored the travel of the Indian team to the IOL. I accompanied the team as one of the team leaders.
This year, round 1 took place in January and approximately 150 students wrote the test. Microsoft Research again organized and hosted the round 2 camp, which was held May 24–31, and we will sponsor the trip of one of the Indian teams to the IOL. (Our friends at the Xerox Research Center India are underwriting half the cost of the second team.) Next year, India will host the IOL, which is being hosted in Bulgaria this year.
The Panini Linguistics Olympiad medal winners: juniors in the front row and seniors in the middle row—the seniors will represent India at IOL this year. Tutors and organizers are in the back row.
In short, we are promoting the Linguistics Olympiad in every possible way: by getting more institutes, people, and companies involved; by promoting awareness among students and schools through various events; by funding and organizing the round 2 camp and IOL travel; and by getting involved with the technical activities, such as designing problems, delivering lectures, and coaching the students post-selection. We are already witnessing a very promising pattern: many Indian participants are choosing linguistics for their university studies, and even those who gravitate to other disciplines (mostly computer science) pursue linguistics or languages as a minor.
It is our hope that these efforts enhance the scientific study of language in India and around the world.
—Monojit Choudhury, Researcher, Microsoft Research