Invited Talks

At SERI 2026, we are excited to present the following invited talks:

Dr. Diptikalyan Saha

Affiliation: Senior Technical Staff Member and Master Inventor, IBM Research India Talk Title: Mainframe Application Reliability in the Agentic AI Era Abstract: Enterprise mainframe applications still run the core systems of banks, insurance companies, retailers, and governments. Reliability in these systems is a business necessity. At the same time, Agentic AI is changing how software is developed, tested, operated, and maintained. This talk explores how runtime insights and human expertise can be combined with AI agents to improve reliability across large mainframe ecosystems and derisk against the decline in mainframe skills. The first part of the talk focuses on Functional Reliability through AI-driven test generation for COBOL applications. While Large Language Models (LLMs) have shown remarkable capabilities in generating test cases, they often miss deep language semantics and COBOL edge cases. They also struggle to understand environment and resource behavior. Many approaches work for small programs but fail for large enterprise applications. This talk presents our experience in grounding LLMs using runtime behavior and execution feedback. We discuss how optimized feedback from controlled execution can improve the quality and reliability of generated tests. The second part focuses on Operational Reliability through Agentic AI for AIOps for root cause analysis. Enterprise systems generate huge volumes of logs, alerts, operational messages, and failure signals. Diagnosing failures in such systems is difficult and time consuming. We discuss how AI agents can combine causal reasoning, enterprise knowledge, and human expertise to investigate incidents and identify probable root causes. The talk also highlights how these ideas are being incorporated into the IBM Z AIOps portfolio to improve operational resilience for enterprise mainframe systems. Bio: Dr. Diptikalyan Saha is a Senior Technical Staff Member and Master Inventor at IBM Research India. His research spans Artificial Intelligence, Software Engineering, Program Analysis, Software Testing, Verification, and AI Trustworthiness. His current work focuses on AI-driven software testing, testing AI systems for robustness and fairness, and improving reliability in enterprise-scale software systems. He received his Ph.D. in Computer Science from the State University of New York at Stony Brook and his B.E. in Computer Science and Engineering from Jadavpur University. Google Scholar

Dr. Chetan Arora

Affiliation: Director of Education, Software Systems and Cybersecurity, Monash University Talk Title: Prompt. Pray. Deploy. — The Agentic AI Wake-Up Call for Requirements Engineering Abstract: Welcome to the age of Agentic AI: systems that don't just predict or generate, but plan, act, use tools, and pursue goals across multiple steps with startling independence. It's genuinely exciting. It's also, from a software engineering perspective, a little terrifying. Over the past several years, my research has been chasing a moving target. At first, the question was whether RE knew how to deal with AI systems at all. Could we specify systems that learned, adapted, and behaved undeterministically? Then GenAI changed the direction of travel. AI was no longer just the system being specified; it was becoming a participant in the RE process itself, helping elicit needs, draft specifications, analyse ambiguity, and, yes, hallucinate with tremendous confidence. More recently, we studied the ethical risks of deploying generative AI, and a pattern has become hard to ignore: our mitigations often arrive after the behaviour has already escaped the specification. Agentic AI pushes this problem further. In this talk, I'll share what I think is the central missing piece in how we specify, build and govern agentic systems today: a clear, explicit boundary around delegated autonomy. Not buried in a prompt. Not implied by a tool schema. Specified, reviewed, and owned. This isn't about slowing down AI adoption. It's about making sure the systems we're unleashing are ones we'd actually stand behind. Because an agent that acts without a proper specification isn't autonomous. It's just unsupervised. Bio: Dr. Chetan Arora is Director of Education for Software Systems and Cybersecurity at Monash University, Australia, and an internationally recognized researcher in Requirements Engineering, Artificial Intelligence, and computing education. His research focuses on specification-driven AI systems, AI governance, safety-critical software engineering, and regulation-ready AI methodologies for domains including healthcare, cybersecurity, and space systems. He serves as the Oceania representative on the International Requirements Engineering Board (IREB) and has received multiple best paper awards in Requirements Engineering. Google Scholar

Prof. KC Sivaramakrishnan

Affiliation: Assistant Professor, Indian Institute of Technology Madras (IIT Madras) Talk Title: From Convergence to Confidence: Push-Button Verification for Replicated Data Types Abstract: Replicated Data Types (RDTs) underpin a growing class of geo-distributed applications, but what it means for an RDT to be correct, and how to prove it, remains surprisingly subtle. Strong eventual consistency guarantees only that replicas eventually agree; replication-aware linearizability further requires that whatever state they agree on is reachable by linearising the updates each replica has actually observed. A compelling specification, but one that has historically demanded painstaking, hand-written proofs. In this talk, I will trace a multi-year arc aimed at replacing those proofs with push-button verification for Mergeable Replicated Data Types (MRDTs). Automated proof assistants and, more recently, agentic proof-oriented programming are steadily eroding the need for manual scaffolding. The story, I hope, illustrates something broader: that the gap between "we believe this merges correctly" and "we have proved it merges correctly" is narrowing to the point where correct-by-construction replicated data is becoming a realistic engineering proposition rather than a research aspiration. Bio: Prof. KC Sivaramakrishnan is an Assistant Professor in the Department of Computer Science and Engineering at IIT Madras and the Chief Technology Officer of Tarides. His research interests span programming languages, concurrency, distributed systems, formal verification, and functional programming. He is best known for leading the Multicore OCaml project, which introduced native support for concurrency and parallelism into the OCaml programming language and formed the basis of the OCaml 5.0 release. Prior to joining IIT Madras, he was a Senior Research Associate at the University of Cambridge Computer Laboratory, an 1851 Research Fellow, and a Research Fellow at Darwin College, Cambridge. He received his M.S. and Ph.D. in Computer Science from Purdue University and his B.E. in Computer Science and Engineering from Anna University. Google Scholar

Rishiyur Nikhil

Affiliation: CTO and Co-Founder, Bluespec, Inc. Talk Title: Bringing Unity to Software and Hardware Engineering Abstract: The importance of hardware accelerators has increased steadily. Examples include floating point (decades ago), TCP/IP offload, encryption, security, and, today, AI training and inference. The importance is compounded by the flattening of Moore and Dennard scaling, requiring an organic, unified approach to software and hardware design. Each complex hardware unit, whether CPU or accelerator, is best viewed as a concurrent, distributed system, even though it may span just a few millimeters. A system of CPU(s) and accelerator(s), in turn, is also best viewed as a concurrent, distributed system. This is for maximum flexibility in microarchitecture, profound affecting tradeoffs between performance, silicon resources and energy. In this talk we elaborate on this unifying programming model, drawing on decades-old roots--Guarded Commands [Dijkstra 1976], UNITY [Chandy and Mishra 1988], Concurrent Sequential Processes [Hoare 1978], and others. Bio: Rishiyur Nikhil is CTO and co-founder of Bluspec, Inc., where he promotes high-level languages and methodologies for the design and verification of complex digital hardware. He is a key contributor to the BSV and BH open-source High-Level Hardware Design Languages and their applications, which use ideas from Haskell and atomic rule-based specs. He has created several open-source RISC-V CPU and System designs, and chaired the RISC-V Foundation's technical group that selected the RISC-V ISA formal spec in Sail. His degrees are from U. Pennsylvania (CS MSEE and PhD) and IIT Kanpur (EE BTech). His interests and R&D career (at MIT, Digital Equipment Corp. and some startups) span full systems, from formal methods and high-level programming languages to CPUs and system micro-architectures.

Aditya Vempaty

Affiliation: Research Scientist, Emergence AI Talk Title: Verified Autonomy: Why Large Language Models Alone Aren't Enough, and What a Neuro-Formal Stack Looks Like Abstract: Large language models have gotten astonishingly good at short, exam-style tasks, but the moment we ask them to operate autonomously over long horizons, to compose across agents, or to touch systems where a bad decision costs millions, they fail in ways that no amount of scaling seems to fix. Emergence AI's recent *Emergence World* study makes this concrete: give ten agents fifteen days in a live, tool-grounded world and some frontier models collapse entirely, some drift into rubber-stamp governance, and, most sobering, populations of well-behaved agents can be *contaminated* into rule-breaking by a single misaligned peer. The relevant unit of safety is the deployed system, not the model. In this talk, we argue that closing this gap requires a **neuro-formal** stack: LLMs handle proposal, negotiation, and natural-language interfaces while formal methods - SMT solvers, proof assistants, verified kernels — hold the load-bearing correctness guarantees and surface actionable diagnostics when the world violates assumptions. We'll show how we've been learning to build this stack by grounding it in real domains: **airline irregular-operations recovery**, where a Z3 pre-feasibility gate and Lean 4 proven repair functions turn a silent 1.5-second wrong answer into a 20-millisecond unsat core with concrete relaxations; and **semiconductor post-silicon test-data analysis**, where a 69-rule Lean 4 kernel lifts an LLM's bug-detection recall from ~0.60 to ~0.97 and, critically, *widens* that gap as bugs interact — a knowledge gap that a stronger model does not close. We'll close with early results from a general-purpose verifiable code-generation tool, which turns natural-language requirements into pip-installable Python packages whose core components carry Dafny or Lean proofs into runtime precondition enforcement. Bio: Aditya Vempaty is a Research Scientist at Emergence AI, where he works on verified autonomous systems, combining large language models with formal verification methods to build agents that are provably correct in the domains where correctness matters. His current work spans a general-purpose verifiable code-generation pipeline, a Lean-4 kernel for semiconductor post-silicon analysis, a neuro-formal recovery system for airline irregular operations, and *Emergence World* — a long-horizon multi-agent evaluation platform. Prior to Emergence AI, Aditya held research role at IBM Research, and holds a Ph.D. in Electrical Engineering and Computer Science from Syracuse University. He has published widely on machine learning, human–AI collaboration, and inference over noisy signals, and co-authored the book *Secure Networked Inference with Unreliable Data Sources* (Springer, 2018).