Manos Kapritsos earns CAREER Award to apply formal reasoning to software performance

Prof. Manos Kapritsos has earned an NSF CAREER Award to extend the use of formal verification techniques and provide guarantees that software systems will meet performance expectations. The project aims to apply logical methods currently used to verify a program’s correct execution to additionally produce guarantees about things like execution time and latency. The work will focus in particular on large, complex, distributed systems that are difficult or impossible to test fully with existing methods.

“In practice a system’s performance is just as critical as its correctness and developers spend much of their time understanding and debugging it,” said Kapritsos. While research has already progressed quite far on applying formal methods to software bugs related to incorrect execution (including work by Kapritsos and his collaborators), the application of these techniques to a system’s performance has been left largely unexplored.

Currently, developers use techniques such as logging, tracing, and profiling to identify performance problems. These techniques not only lack guarantees that their results are thorough and accurate, but they also require either a full deployment of the system for testing or can only identify bugs after they’ve begun to wreak havoc.

The proposed research will develop a set of methodologies to comprehensively reason about all aspects of a system’s performance. Kapritsos hopes that it will provide developers with an alternative way of understanding the performance of their system: reasoning about it formally before they even deploy it.

This project is part of Kapritsos’ larger goal of bringing formal verification to developers and other practitioners. Currently, the techniques are viewed as too difficult and time consuming to be viable at a large scale. But formal verification is critical to building systems that are guaranteed to be safe and high-performance. By focusing on performance, Kapritsos aims to bridge a significant gap in existing verification techniques. This will lead to more reliable and more cost-effective services for end users.

“Bringing formal verification to the real world, however, is not just about research,” said Kapritsos. “It is equally important to educate the developers about the benefits and the proper use of formal verification and to dispel the notion that these techniques are the academic equivalent of ‘rocket science’—an intellectually challenging task left to a small number of experts.”

Kapritsos has already begun the effort to raise awareness and increase the accessibility and impact of formal verification techniques by organizing an annual Summer School on the verification of systems software. Additionally, he is co-authoring a book titled ”Formal Verification for Practitioners.” Kapritsos and his co-author hope that this book will serve as the primary reference on how to apply formal verification techniques to real-world systems. The book is intended to be used as a textbook for verification-oriented programming courses as well as a manual for more experienced developers.