About
I am a researcher with more than twelve years of experience in automated reasoning and system software development. My broad research focus is on solving software engineering problems through learning and logic.
I did my Ph.D. under the guidance of Deepak D’Souza at IISc. During my Ph.D., I worked on synthesis of program proofs that help in formal verification of programs 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 Mandayam Srivas. Long before that, I was a network-based storage system developer at NetApp for five years.
You may contact me at: 
Publications
Please refer to dblp for the latest papers.
| 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 |
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: FASE24, FMCAD23, CAV22, FSTTCS22, FMCAD21, TACAS22 AEC, PLDI21 AEC
- Talks: PLDI21; FMCAD20; FSTTCS20,23; SAS18; TACAS24; ESOP24; FMUpdate18,19,21; SAT-SMT School22