Keynote: The Future of Software Engineering

Formal Methods (FM), which are based on precise mathematical principles, have always held the promise to change the way that software systems are developed. Now the time has come: with modern language and tool support FM will impact every stage of the development process including requirements, specification, design, implementation, testing, and even documentation. But what has enabled this sudden breakthrough of FMs and what comes next?

The last 10 years have seen amazing progress in scalability and widespread availability of basic formal methods infrastructure like model checkers, automatic theorem provers, standardized intermediate languages, compiler infrastructure, etc. This basic infrastructure has also enabled the amazing success story for the wide spread adoption of static and dynamic program analysis tools. 10 years ago, static program analyses were imprecise and slow. In addition they often required adding complex annotations. We can remove this impediment by using other artifacts like existing assertions, tests, and even earlier code versions as specifications against which the implementations are checked. In fact, users of modern program analysis tools often don’t even recognize that formal methods are used under the hood.

The next 10 years will see the wide adoption of lightweight FMs, which emphasize partial specification and focused application, but for other phases than just implementation and testing. For instance, going to the cloud requires new ways to protect data and privacy. Logic based policy languages can fill this hole. The increasing complexity of modern software/hardware systems requires that we need to analyze these systems at design time, since it will simply be too expensive to build the wrong thing. New constraint-based languages are already emerging that support these analysis. But of course computer scientists’ ultimate dream is to teach the computer to program itself. Can FMs help realize this dream, too?

Speaker Details

Wolfram Schulte is a principal researcher and the founding manager of Microsoft’s Research in Software Engineering (RiSE) team in Redmond, Washington. His research concentrates on improving software development. At Microsoft he co-designed runtimes like Linq and the Task Parallel Library, test tools like Spec Explorer and Pex, verifiers like Spec# and VCC, and modeling tools like AsmL and Formula. Schulte has coauthored more than 80 refereed papers, and holds numerous patents. He has a PhD from TU Berlin, a state doctorate from the University of Ulm, and he worked for a couple of years as a software engineer.

Date:
Speakers:
Wolfram Schulte, Peli de Halleux, and Nicholai Tilman
Affiliation:
Manager, Software Engineering, Microsoft Research, Redmond, USA, Microsoft
    • Portrait of Jeff Running

      Jeff Running

    • Portrait of Wolfram Schulte

      Wolfram Schulte

      Partner Group Software Engineering Manager