Formal Systems Laboratory

About Me

• I am a sixth-year Ph.D. student advised by Professor Grigore Rosu, working closely with Professor Madhusudan Parthasarathy as well. I am interested in techniques for automated program verification, with a focus on Matching Logic and First-Order Logic (with least fixpoints).

Publications

• Towards A Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic (OOPSLA’20)
• A First-Order Logic with Frames (ESOP/ETAPS’20)
• Foundations for Natural Proofs and Quantifier Instantiation (POPL’18)
• Program Verification by Coinduction (ESOP/ETAPS’18)
• Towards a Verified Model of the Algorand ConsensusProtocol in Coq (FMBC’19)
• Verifying Finality for Blockchain Systems (CoqPL’19)