Bridging Logic and Language: Program Verification in the LLM Era

Title of the Talk:Bridging Logic and Language: Program Verification in the LLM Era
Host Faculty: Dr.Ramakrishna Upadrasta
Speaker: Dr Subhajit Roy
Date: 21 May 2026
Time: 12:00noon – 1:00 pm

Abstract
Program verification has stood as one of the enduring challenges in computer science. Despite decades of progress, many verification problems remain beyond the reach of even the most advanced verification engines. A central difficulty lies in the need for human insight—the ability to identify the right invariants, ranking functions, or proof strategies that make verification succeed. While numerous heuristics have been developed to approximate this reasoning, the gap has persisted.

In our work, we ask a simple but powerful question: Can Large Language Models provide these missing insights? We explore how the creative reasoning capabilities of LLMs can be combined with the precision and rigor of formal methods—developed and refined over the past half-century—to advance the automation frontier in verification.

This talk will present our recent efforts in using LLMs to infer proof artifacts such as inductive invariants for correctness and ranking functions for termination, to refactor code for migration into memory-safe dialects of C, and to learn idiomatic templates for what we call “angelic verification.”

We believe that the convergence of LLMs and formal verification represents a promising new direction—one that could transform how we approach the problem of proving programs correct.

Bio
Subhajit Roy is currently the Jainendra Navilakha Chair Professor in the Department of Computer Science and Engineering at the Indian Institute of Technology Kanpur (IIT Kanpur), where he has been a faculty member since 2010. His research interests span programming languages, software engineering, and formal methods, with recent interest in the verification and transpilation of quantum programs.