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?