CAREER: Formal Verification of Performance Properties for Distributed Systems

n our daily lives we increasingly depend on computers: from our emails and our work meetings, to social media and interacting with our friends and family. The computer systems that provide us these services are not only vast in size, but also complex and subtle. A single component being slower than expected can drive the entire system into unpredictable and catastrophic behaviors that result into the entire system being unavailable for long periods of time, disrupting all services—human and automated—that depend on it.

For the longest time, the research community has been trying to understand the performance of these complex systems in a best-effort way: deploying the system and observing its behavior in a number of test scenarios. The complexity of these systems, however, makes it impossible to thoroughly test everything that can go wrong. Inevitably some corner case emerges which drives our deployed system to its knees and we discover—too late—that our testing was not thorough enough.

This proposal puts forward a rigorous way of reasoning about the performance of our systems: leveraging the recent advances in formal reasoning to allow programmers to systematically develop rigorous guarantees about the duration and speed of the system’s executions.

This proposal aims to solidify the foundation on which our future systems will be built. It uses formal reasoning to provide guarantees—not expectations—about how our systems will behave in practice. For the end users this means that the computer services they use every day will be more cost-effective and more reliable.

Achieving these benefits, however, requires more than research. The proposal puts forth an educational plan for bringing verification closer to practicality by introducing it to current and future engineers by means of a new class on verification, an ongoing verification summer school, and a book on how to apply formal verification to real-world systems.

Together, the research and educational objectives of this proposal aim to make formal reasoning an integral part of computing. If the everyday user is to put their trust in our computer systems, those systems need to be more than just tested; they must be provably correct.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.