Publications
-
Syndicate: Synergistic Synthesis of Ranking Function and Invariants for Termination Analysis
Yasmin Chandini Sarita, Avaljot Singh, Shaurya Gomber, Mahesh Viswanathan, Gagandeep Singh
Submitted for review at PLDI '24
TLDR: Developed a framework that proves termination of programs by synthesizing ranking function and loop invariants simultaneously.
-
Enabling Type-Cast Operations in SMT with Efficient Oracle Encodings
Shaurya Gomber, Kevin Cheang, Dejan Jovanovic, Andrew Reynolds, Amit Goel
Planned for submission at CAV '24
TLDR: Developed efficient oracles and SMTO encodings to encode type-casting semantics in SMT.