New Associate Professor develops verification techniques to ensure correctness of software

Errors in software systems are pervasive. Regardless of the scale of the problem, they affect our everyday lives. A recent example is a problem in electric Lime scooters that has led to injuries of users worldwide. Also, an error in Java’s standard sorting algorithm demonstrates that software errors can remain undetected despite widespread usage and are part of today’s programming reality.  

- Frequently, software bugs occur due to the complexity of software, more specifically due to a lack of understanding of all the corner cases in it. I believe that the only sustainable way to develop software that has no such errors is to use verification tools, says Associate Professor Dmitriy Traytel.

He explains that, traditionally, algorithms have been proven correct on paper. But at some point, humans cannot handle the increasing complexity of programs anymore.

- To tame this complexity, computers themselves can help. Some verification tools can prove programs correct (semi-)automatically, others can check the correctness of an argument made by humans, says Dmitriy.

Verifying programs in two ways

Dmitriy Traytel’s research focuses on two areas: Runtime verification and interactive theorem proving.

Runtime verification focuses on ensuring that running systems comply with the rules that they should follow. Techniques for doing so are available for and used by most companies today, often in form of log monitoring. Dmitriy works on improving these techniques to scale up to handle huge quantities of data produced by the running systems.

Interactive theorem proving is concerned with carrying out machine-checked proofs and developing the systems that check these proofs: proof assistants. Beyond simply checking human-written proofs, a proof assistant supports its users in constructing these proofs. It will not accept a faulty or imprecise argument, thereby providing the highest levels of trustworthiness.

Worth the effort

Landmark achievements in interactive theorem proving include realistic verified compilers, operating systems, and distributed systems. Dmitriy works on making proof assistants more expressive and easier to use.

- Proving a program correct in a proof assistant is a significantly more heavy-weight task compared to using a runtime verification tool. This is because one has to consider all the possible behaviours that the program may exhibit. In contrast, in runtime verification only focuses on a single program execution. However, proof assistants are worth the effort because they provide a much stronger guarantee about the program than runtime verification, Dmitriy explains.

Dmitriy’s preferred proof assistant is called Isabelle. According to him, Isabelle is arguably the most user-friendly proof assistant, and one that balances expressiveness and automation very well.

For now, proof assistants are still a technology of tomorrow. Only giant corporations like Amazon, Apple, Intel, or Microsoft have the resources to use them for everyday software development. It is Dmitriy’s goal to contribute to making these techniques easy to use and accessible to everybody who wants to develop error-free programs.