Computers are everywhere, controlling everything from phones and traffic lights to airplanes and buildings. And inside each computer is software: line after line of complex code that tells the program, and any attached hardware, what to do.
It’s amazing how the world has come to rely on software.
Testing is a vital step in software development, but it’s hard to test every possible path through millions of lines of code. For example, in 2003 the northeastern United States and Canada experienced a blackout that affected more than 50 million people due to an obscure problem in the energy management system software. It was admitted afterwards that even extensive testing would not have found this problem. So we need more formal methods to determine such program behavior in advance. This software verification—the science of deducing whether a program will execute correctly—is crucial for reliability in complex programs.
Microsoft Research Podcast
AI Frontiers: AI for health and the future of research with Peter Lee
Peter Lee, head of Microsoft Research, and Ashley Llorens, AI scientist and engineer, discuss the future of AI research and the potential for GPT-4 as a medical copilot.
Much of the existing work in software verification does not consider the processor design itself, which is a problem because new multi-core processors and more complex computer architectures are being designed for next-generation computing platforms—from mobile phones and tablet devices to cloud computing data centers. A new collaboration between Koç University (opens in new tab) in Turkey, Microsoft Research, and the Barcelona Supercomputer Centre (opens in new tab) is taking a unique multidisciplinary approach, bringing together world-leading researchers in computer architecture, formal methods, and systems to produce a coherent, end-to-end, robust methodology for computer architecture design.
Dr. Serdar Tasiran from Koç University leads the discussion with his research team:
Hassan Salehe Matar, Cansu Erdogan, Umit Can Bekar, Omer Subasi, Zeynep Su Kurultay, and Emre Gul.
Research leader at Koç University, Serdar Taşıran (opens in new tab), is excited about this new project, “After working together for many years, it is tremendous that we are beginning this formal collaboration between Microsoft Research and Barcelona Supercomputer Centre to look at the whole problem of software verification from the processor-up.” This follows a strong history of working closely with Microsoft Research in Redmond, Cambridge, and India.
The team aims to create a holistic, robust approach to the development of novel computer architectures. This is required to simultaneously push the state-of-the-art while permitting application-driven scenarios to be taken into account at an early stage in the hardware design.
Tim Harris (opens in new tab), a senior researcher at Microsoft Research Cambridge, explains “Modern programming languages such as F# rely on multiple layers of software for activities such as garbage collection and managing parallel work items. This collaboration will help us develop new hardware techniques to accelerate these activities, while ensuring that the correctness of programs is not compromised.”
Mateo Valero (opens in new tab), director of Barcelona Supercomputing Center, adds, “This collaboration simultaneously targets the three requirements that modern multi-core computing faces today: processors should be fast and efficient, they should be easy to program, and they should compute in a verifiable and correct way.”
Fabrizio Gagliardi (opens in new tab), director of Microsoft Research Connections Europe, the Middle East, and Africa (EMEA), is delighted. “This is a strong partnership that brings together world experts in software verification and computer architecture to solve this hugely challenging problem,” he says. “We look forward to this project paving the way to more reliable software on tomorrow’s hardware.”
—Kenji Takeda (opens in new tab), Solutions Architect and Technical Manager, Microsoft Research Connections EMEA
Learn More