Curriculum vitae

Work Experiences

• Graduate Research Assistant, Rochester Institute of Technology (Aug '24–Present)
  • Working under the supervision of Prof. Arthur Azevedo de Amorim.
• Project Assistant, Indian Institute of Technology Gandhinagar (Aug '23–Aug '24)
  • Worked under supervision of Prof. Abhishek Bichhawat on the DY* framework to prove properties of group messaging protocols.
• Intern, AlgoLabs Chennai Mathematical Institute (Apr '22–Apr '23)
  • Worked under contract with SupraOracles, under supervision of Prof. M Praveen. We worked on verification of distributed protocols in Microsoft Ivy. This extended to my M.Sc. thesis.

Research Experience

• Proving Safety of SupraBFT using Microsoft Ivy (M.Sc. thesis)
  • Under supervision of Prof. M Praveen. Slides, dissertation, repo

Teaching Experience

• Teaching Assistant, Software Verification and Analysis (Jan–Apr '23)
  • Course offered by Prof. M K Srivas. I mainly took lab sessions, demonstrating the usage of CBMC, Frama-C (Eva, WP), UCLID5, and Z3 (SMT-LIB)

Schooling

• PhD in Computing and Information Sciences (2024–Present)
  • Rochester Institute of Technology
• M.Sc. in Computer Science (2021–2023)
  • Chennai Mathematical Institute
• B.Sc. (Hons. in Computer Science) (2016–2020)
  • Sonarpur Mahavidyalaya, affiliated to the University of Calcutta

Talks

• Relational Cryptis: A Separation Logic for Indistinguishability in the Symbolic Model, Upstate PL Seminar 2026
  • Abstract

    Cryptographic protocol verification in the symbolic model in the style of Dolev and Yao has seen significant advances lately. Tools such as ProVerif, Tamarin, and DY* have seen tremendous success in proving various trace properties of various complex and layered protocol designs. While trace properties has been a success story, the other big class of properties, namely the hyperproperties, has not seen much development in the symbolic model. Current tools can only verify elementary protocols with various restrictions on the protocol code.

    We extend Cryptis, a separation logic built on top of the Iris framework to reason about symbolic cryptography, to the hyperproperty setting. We show the IND-CPA game implemented using this 'relational Cryptis'. We then sketch how relational Cryptis might be used in the verification of larger protocols and how such code and their proofs might compose within relational Cryptis, and with other logics built on top of Iris.

  • Slides, repo
• Simple As Possible – Computers, STEMS Qualifier Camp (Apr '23)
  • Talk on digital electronics and computer architecture, given jointly with G Namratha Reddy.
  • Main slides, additional slides, repo

Service

• Reviewer
  • JITA 2025