Keynote Talk : Automated Reasoning for Weak Consistency

Suresh Jagannathan Purdue University (USA)

ABSTRACT: Modern distributed applications often replicate data across geographically diverse locations to enable trust decentralization, guarantee low-latency access to application state, and provide high availability even in the face of node and network failures. Replication complicates program reasoning, however, since not all copies of an object are guaranteed to hold the same state at the same time.  Existing verification approaches impose a high cognitive burden on developers to establish necessary invariants and derive sophisticated proof strategies to ensure application correctness in these environments.  In this talk, I describe several techniques to enable automated verification of distributed applications in the face of weak-consistency that greatly alleviates this burden.  Our solutions employ new logical specification formalisms, novel symbolic execution and model-checking abstractions, and tailored static analyses that collectively enable the construction of trustworthy (geo-replicated) distributed applications, without requiring extensive programmer involvement to enable verification.

BIOGRAPHY: Suresh Jagannathan is the Samuel D. Conte Professor of Computer Science at Purdue University.  His research interests are in programming languages generally, with a specific focus on program verification, functional programming, and concurrent and distributed systems.  From 2013 – 2016, he served as a program manager in the Information Innovation Office at DARPA, where he conceived and led programs in probabilistic reasoning and machine learning, program synthesis, and adaptive computing.  He has also been a visiting faculty at Cambridge University, where he spent a sabbatical year in 2010; and, prior to joining Purdue, was a senior research scientist at the NEC Research Institute in Princeton, N.J. He received his Ph.D from MIT.