Microsoft Research Blog

The Microsoft Research blog provides in-depth views and perspectives from our researchers, scientists and engineers, plus information about noteworthy events and conferences, scholarships, and fellowships designed for academic and scientific communities.

IEEE Computer Society honors Wolfram Schulte for research leadership, contributions to program verification

February 29, 2016 | By Microsoft blog editor

By George Thomas Jr., Writer, Microsoft

Software verification — the crucial process of assuring programs perform as expected — may not be top of mind for most of us.

But considering its role in the development of just about anything based on software — which seemingly is nearly everything these days — its importance cannot be understated.

And that’s where Wolfram Schulte comes in.

Wolfram SchulteIn his nearly two decade-long career at Microsoft, Schulte has made significant contributions to software development, including building program verifiers like Spec# and VCC, two widely used verification tools for programming in the C# and C environment, and Pex, an automated unit testing tool for the .NET environment built on verification technology.

On Monday, Institute for Electrical and Electronics Engineers announced that Schulte was selected to receive the IEEE Computer Society 2016 Harlan D. Mills Award. The award honors Schulte’s research and research leadership contributions, which have led to major theoretical and practical advances in software verification.

“I am so humbled that the committee selected me for this prestigious award,” Schulte said. “I am still in absolute awe of the scientific work of earlier Mills awardees, including Mills himself. I never imagined being among them.”

Schulte joined Microsoft in 1999.

In 2008, he founded the Research in Software Engineering Group (RiSE), a research group that focuses on bringing the latest software engineering advances to Microsoft’s business. RiSE developed many foundational pieces for software verification. For instance, Z3, a high-performance automated theorem prover, won the ACM SIGPLAN Award in 2015.

Then, in the summer of 2012, he founded the Tools for Software Engineers team, a product team that focuses on speeding up software development by working through issues such as code review, build, test and automated programming analysis.

He is currently serving as a director of engineering for Microsoft’s Cloud and Enterprise division.

Schulte’s career at Microsoft started out as a happy coincidence. At one time, he said he hadn’t even considered a career outside of academia.

“I worked at a German university wanting to become a tenured professor,” he said.

But when a colleague asked if he wanted to interview with Microsoft, he said, “I figured, why not? I have some time to kill.”

Some 16 years later, Schulte said he’s stayed at Microsoft because of the opportunity to work on some of the toughest problems in computer science with the smartest researchers and product engineers he knows.

“And it’s the impact,” he added. “Hopefully changing the world of a billion users for the better.”


Tools for Software Engineers

Research in Software Engineering

Yong Rui wins IEEE Computer Society 2016 Technical Achievement Award

Up Next

Programming languages and software engineering

Researchers work to secure Azure Blockchain smart contracts with formal verification

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 an understatement. According to Gartner, the technology is positioned to […]

Microsoft blog editor

Programming languages and software engineering

Project Everest: Reaching greater heights in internet communication security

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 verification tools and techniques the Everest team is using and developing, is the first in a series exploring the groundbreaking work, which is available on […]

Microsoft blog editor

SPACER and Z3: Accessible, reliable model checking as theorem proving

Mathematics, Programming languages and software engineering

SPACER and Z3: Accessible, reliable model checking as theorem proving

“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 – this is the terminology occupying the research space of computer […]

Nikolaj Bjorner

Principal Researcher