User-Friendly Formal Methods

Computers have made many aspects of modern life much easier, but what happens when things go wrong, and how can we prevent it from happening?

Almost all parts of modern life involve computer programs, from banking, insurance and taxes to social networks, dating apps and instant messengers. All of these applications rely on complicated software to work and move information between your device and the billions of other computers on the planet. On a normal day, we barely notice any of this, but when computers do something wrong, everything can fall apart within seconds.

Large companies stand not only to lose millions in revenue for every minute their programs are broken, but also to take potentially devastating blows to their reputation when their services are down for even a few hours or when they leak data about their users. In some industries, such as aviation and medical devices, the reliability of computer programs can even be the difference between life and death.

Software developers have traditionally attempted to avoid errors by testing their programs in a variety of situations, adding new tests whenever an error is discovered such that the newly discovered error never happens again without them noticing. The problem with this approach is that errors will always slip through the cracks since it is, in most cases, impossible to test all possible situations. To avoid this problem, researchers in the field of formal methods have for many years worked on tools and methodologies that can prove programs correct using mathematics and logic. Unfortunately, industrial usage of these tools is generally limited. While some tools such as type systems for programming languages have become mainstream, others are difficult to use and have therefore mostly been adopted in highly specialized domains such as aviation, where safety is the first priority.

The goal of this project is to design new tools and components that make formal methods easier to use for the average software developer. The project focuses on distributed systems, which involve multiple programs communicating and coordinating with each other, making the programs even harder to test than usual. By designing more user-friendly tools, the hope is to turn the tide and give formal methods a reputation for making software development easier, faster and safer.

With software that is proven correct instead of simply tested in some specific situations, even the most complicated programs can stay behind the scenes, and we can keep using the apps and websites they support without worrying that things might go wrong.