Suresh Jagannathan

Suresh Jagannathan

Professor Suresh Jagannathan is interested in the semantics and implementation of high-level programming languages. His work focusses on formal methods for describing and implementing such languages, e.g., type theory, program analysis, abstract interpretation, etc., as well as compiler and runtime techniques that leverage such analyses. He also has an active interest in the specification, verification, and implementation of concurrent and distributed systems. Much of this work involves exploring the role of verification techniques to enable sound program optimizations for concurrent programs. Certified compilation of expressive concurrent languages is another subject being actively pursued. An important sub-topic is the definition of expressive memory models that define visibility and consistency guarantees on shared data accesses. Lifting processor-defined memory consistency properties to inform compilation and language specification is an important focus area.

  1. Zhu, H., Petri, G., Jagannathan, S., Automatically Learning Shape Specifications, ACM Conference on Programming Language Design and Implementation, pp. 491-508, 2016.
  2. Zhu, H., Nori, A., Jagannathan, S., Learning Refinement Types, ACM International Conference on Functional Programming, pp. 400-411, 2015.
  3. Zhu, H., Nori, A., Jagannathan, S., Dependent Array Type Inference from Tests, International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 412-430, 2015.
  4. Sivaramakrishnan, K., Kaki, G., Jagannathan, S., Declarative Programming over Eventually Consistent Data Stores, ACM Conference on Programming Language Design and Implementation, pp. 413-424, 2015.
  5. Petri, G., Vitek, J., Jagannathan, S., Cooking the Books: Formalizing JMM Implementation Recipes, European Conference on Object-Oriented Programming, pp. 445-469, 2015.
  6. Sivaramakrishnan, K., Kaki, G., Jagannathan, S., Taxation Without Representation: A Uniform, Low- Overhead, and High-Level Interface to Eventually Consistent Key-Value Stores, IEEE Data Engineering Bulletin, pp. 52-64, 2016.
  7. Dodds, M., Jagannathan, S., Parkinson, M., Svendson, K., Birkedal, L., Verifying Custom Synchronization Constructs in Higher-Order Separation Logic, ACM Transactions on Programming Languages and Systems, 38(2):4, 2016.
  8. Zhu, H., Petri, G., Jagannathan, S., Poling: SMT-Aided Linearizability Proofs, Computer Aided Verification, pp. 3-19, 2015.
  9. Samak, M., Ramanathan, R., Jagannathan, S., Synthesizing Racy Tests, ACM Conference on Programming Language Design and Implementation, pp. 175-185, 2015.
  10. Botinkan, B., Dodds, M., Jagannathan, S., Proof-Directed Parallelization Synthesis by Separation Logic, ACM Transaction on Programming Languages and Systems, 35(2):8, 2013