Colloquium Details

Secure Data-Intensive Applications through Automatic Formal Reasoning

Speaker: Gowtham Kaki, Purdue University

Location: 60 Fifth Avenue 150

Date: March 11, 2020, 2 p.m.

Host: Michael Overton


Contemporary online applications are data-intensive, often running on top of large-scale inter-connected geo-distributed databases. The high complexity of these systems coupled with ever-increasing expectations of performance and availability has made it hard for programmers to ensure integrity and safety of data-intensive applications.


In this talk, I demonstrate how techniques rooted in programming languages and automated formal methods can help developers ensure the integrity of data-intensive applications without compromising their runtime performance.  First among such techniques is a method to automatically reason about the safety of non-serializable transactions, which often replace expensive serializable transactions in practice. I show that the semantics of these transactions, albeit non-standard, can be precisely related to the high-level semantics of a database application, making it possible to reason about application safety in the absence of ACID guarantees. Next, I extend this methodology to “weakly-consistent” geo-distributed databases that underlie modern large-scale web services. I present a bounded symbolic execution technique that is effective at identifying and repairing safety violations in realistic distributed database applications. Finally, I present a synthesis technique that can automatically transform ordinary sequential data structures into a class of distributed data structures called Mergeable Replicated Data Types (MRDTs) that can be composed to build linearly-scalable distributed applications. Together, the aforementioned techniques constitute a principled approach towards developing data-intensive applications with strong safety guarantees. I will end the talk with a discussion on the possibility of applying techniques such as these to enforce strong guarantees on an emerging class of distributed applications such as those that enable planet-scale decentralization. 

Speaker Bio:

Gowtham Kaki is a post-doctoral researcher at Purdue University. He completed his Ph.D at Purdue in August 2019 under the supervision of Prof. Suresh Jagannathan. His research is in the areas of Programming Languages and Formal Methods with a focus on automated verification techniques for concurrent and distributed programs. He received several recognitions for his work, including Google’s PhD Research Fellowship (2018), Purdue’s Maurice H. Halstead Award for Contributions to Software Engineering Research (2018), and his alma mater BITS Pilani’s 30-under-30 award (2019).


In-person attendance only available to those with active NYU ID cards. All individuals must show the Daily Screener green pass in order to gain entry to the building.

How to Subscribe