It’s not uncommon for us to hear that the Z3 theorem prover is magical, but the frequency of such complimentary feedback doesn’t make it any less unexpected—or humbling. When we began work on Z3 in 2006, the design was motivated by two emerging use cases:…
In its young existence, the tamperproof and distributed ledger technology blockchain has already generated a lot of buzz and is being seen as disruptive, influencing approaches in such diverse areas as financial services, supply chains, and governance. To say its future is bright might be…
Project Everest is a multiyear collaborative effort focused on building a verified, secure communications stack designed to improve the security of HTTPS, a key internet safeguard. This post, about the high-performance industrial-grade EverCrypt cryptographic provider, is the second in a series exploring the groundbreaking work,…
Spreadsheets are the world’s most widely used programming language, by several orders of magnitude. We asked ourselves whether it would be possible to apply programming language research ideas to make spreadsheets a better programming language? If we could, that would empower a huge user community…
“How can one check a routine in the sense of making sure that it is right?” asked Alan Turing in 1949, foreshadowing the science of program proving decades before it became a formally accepted field of computer science. Program proving, model checking, theorem solving –…
Microsoft MakeCode is a web-based learning environment for kids and teens to create with technology. MakeCode takes a unique approach to computing education by combining the magic of making with the power of code as a way to make learning about computers and technology more…
Ten years ago, while writing a physics engine, I learned about the Barnes-Hut algorithm for the gravitational n-body problem. Normally, computing the Newtonian gravitational forces between n bodies requires evaluations of Newton's law of universal gravitation, as every body exerts a force on every other…
Over the last five years, deep learning-based methods have revolutionised a wide range of applications, for example those requiring understanding of pictures, speech and natural language. For computer scientists, a naturally arising question is whether computers learn to understand source code? It appears to be…
Program synthesis — automatically generating a program that satisfies a given specification — is a major challenge in AI. In addition to changing the way we design software, it has the potential to revolutionize task automation. End users without programming skills can easily provide input-output…
It’s a big shift to change from being motivated by getting published in prestigious conferences and journals, to being motivated by solving real problems for real people. Halfway through my 18-year research career working on program synthesis–the task of automatically constructing a program that satisfies…
Need funding to clear a hurdle in the final stages of your dissertation research? Microsoft Research is offering grants of up to US $25,000 to help a select group of doctoral students cross the finish line and enter the workforce. The Microsoft Research Dissertation Grant…
Halfway through college, I had an identity crisis. Spring was in the air in Hanover, New Hampshire, and my classmates were gearing up for Dartmouth's famed Sophomore Summer term. Most of them would spend much of this term tubing down the Connecticut River, or hiking,…
