Building Verified and Performant Data-Intensive Applications - Alvin Cheung
Workshop on Dependable and Secure Software Systems 2019
From banking to social networking websites, we interact with data-intensive applications every day. Such applications rely on databases for persistent storage, but the separation between the application and the database layer makes it difficult to satisfy end-to-end goals such as performance and correctness. In this talk, I will show how examining the programming system and the database management system in tandem allows developers to build data-intensive applications and systems that are both performant and correct. To illustrate, I will discuss two projects: verified lifting, a methodology that enables applications to leverage optimization exposed by different programming interfaces, and Cosette, a tool for system developers to validate the correctness of their query transformations. Using real-world examples, I will show that these tools enable system builders to reason about the correctness of their optimization, and allow orders of magnitude performance improvement while preserving the same programming interface to the developer.