About
I am a researcher and software engineer with 13+ years of experience building tools that make software more reliable and secure. My work spans static analysis, program verification, taint analysis, and applying ML and LLMs for code reasoning. My goal is to turn research into tools that engineers and security teams can actually use.
I did my Ph.D. under the guidance of Deepak D’Souza at IISc. During my Ph.D., I worked on synthesis of specifications that help in automated program verification using abduction and SMT solving (thesis). I was fortunate to have closely collaborated with Kumar Madhukar and Grigory Fedyukovich during this period. I did my master’s from Chennai Mathematical Institute, where my thesis was done under the guidance of Mandayam Srivas. Long before that, I was an operating system developer at NetApp for five years.
For collaborations, consulting, or opportunities, reach me at: 
Publications
Please refer to dblp for the latest papers.
| PLDI 2026 | Verification Modulo Tested Library Contracts (paper) | Abhishek Uppar, Omar Muhammad, Sumanth Prabhu, Deepak D’Souza, Madhusudan P, Adithya Murali |
| AAAI 2026 (oral 🏆) | On Robustness of Linear Classifiers to Targeted Data Poisoning (paper) | Nakshatra Gupta, Sumanth Prabhu, Supratik Chakraborty, Venkatesh R |
| TACAS 2024 | Weakest Precondition Inference for Non-Deterministic Linear Array Programs (artifact) | Sumanth Prabhu, Deepak D’Souza, Supratik Chakraborty, R. Venkatesh, Grigory Fedyukovich |
| ESOP 2024 | Maximal Quantified Precondition Synthesis for Linear Array Loops (artifact) | Sumanth Prabhu, Grigory Fedyukovich, Deepak D’Souza |
| ATVA 2023 | Automated Property Directed Self Composition | Akshatha Shenoy, Sumanth Prabhu S, Kumar Madhukar, Ron Shemer, Mandayam K. Srivas |
| PLDI 2021 (Distinguished Paper 🏆) | Specification Synthesis with Constrained Horn Clauses (tool, blog) | Sumanth Prabhu, Grigory Fedyukovich, Kumar Madhukar, Deepak D’Souza |
| ICSE (NIER) 2020 | Using hypersafety verification for proving correctness of programming assignments | Jude K. Anil, Sumanth Prabhu, Kumar Madhukar, R. Venkatesh |
| CAV 2019 | Quantified Invariants via Syntax-Guided Synthesis (tool) | Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta |
| FMCAD 2018 | Solving Constrained Horn Clauses Using Syntax and Data (tool) | Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta |
| SAS 2018 | Efficiently Learning Safety Proofs from Appearance as well as Behaviours (tool) | Sumanth Prabhu, Kumar Madhukar, R. Venkatesh |
| TACAS 2018 | VeriAbs: Verification by Abstraction and Test Generation - (Competition Contribution) | Priyanka Darke, Sumanth Prabhu, Bharti Chimdyalwar, Avriti Chauhan, Shrawan Kumar, Animesh Basak Chowdhury, R. Venkatesh, Advaita Datar, Raveendra Kumar Medicherla |
| ATVA 2017 | Concurrent Program Verification with Invariant-Guided Underapproximation (tool) | Sumanth Prabhu, Peter Schrammel, Mandayam K. Srivas, Michael Tautschnig, Anand Yeolekar |
Research Activities
- PC of ATVA 2025
- Keynote talk at ISEC 2025
- Invited talk at CMI
- Invited talk at VSS
- A lecture on CHCs as part of Logic course at IISc
- (Sub-)Reviewer: FSTTCS26, FASE24, FMCAD23, CAV22, FSTTCS22, FMCAD21, TACAS22 AEC, PLDI21 AEC
- Talks: PLDI21; FMCAD20; FSTTCS20,23; SAS18; TACAS24; ESOP24; FMUpdate18,19,21; SAT-SMT School22
Miscellaneous Experiments
- Lean4RuleArena - formally verifying LLM output (contact me for details)
- Soma - ZK circuit repair tool (contact me for details)
- MLIR and Deep Learning Compiler
- Reinforcement Learning for Counterexample
- Sudoku
- Haskell