Mohammad Afzal

About Me

I am a full-time Scientist at TCS Research Pune, India. I completed my PhD under the supervision by Prof. Ashutosh Gupta and Prof. Akshay S at the Department of Computer Science and Engineering, IIT Bombay. I am always open to discussions and research collaborations.

Research Interests

• AI Safety and Formal Verification of Neural Networks
• Explainability of AI Systems
• Runtime Monitoring of AI Systems
• Formal Verification of Programs

Education

PhD (Trustworthy AI), Jan 2020 – Feb 2026
Indian Institute of Technology Bombay, India
Thesis: From Counterexamples to Confidence: Advancing Neural Network Verification

M.Sc. (Computer Science), Jul 2015 – May 2017
Chennai Mathematical Institute, India
Thesis: Property Checking of Array Programs involving Quantification over Array Elements

B.Tech. (Information Technology), Jul 2011 – May 2015
Rajkiya Engineering College, Bijnor (HBTI Kanpur)

Experience

Scientist, Aug 2023 – Present
TCS Research Pune, India

• Led research on robustness verification of deep neural networks.
• Developed scalable verification techniques for ImageNet-scale models.
• Worked on both industrial and PhD-aligned research projects.

Researcher, Jul 2017 – Jul 2023
TCS Research Pune, India

• Designed and implemented verification techniques for array programs.
• Integrated techniques into VeriAbs, winning SV-COMP Gold Medals (2019–2021).
• Reduced ~80% false warnings in large industrial C codebases.

Tools Developed

• DNNV_UF -- A tool for automatically performing formal reasoning about the confidence of neural network predictions.
• DREFINE -- A tool for formally verifying the robustness of neural networks.
• QuantLearn -- A tool for providing explanations of policy demonstrations in the form of LTL formulae.
• VeriAbs -- A tool for verifying C programs.

Publications

Talks

• RHPL@FSTTCS 2025 – Verifying Rich Robustness Properties for Neural Networks.
• SAIV@CAV 2025, OVERLAY@ECAI 2025 – False Positives in Robustness Checking of Neural Networks.
• WCSS@SAT 2024, ATVA 2023 – Using Counterexamples to Improve Robustness Verification.

Professional Service

• Artifact Evaluation Committee: CAV 2023, QEST+FORMAT 2024, TACAS 2024–2026, CAV 2026.
• Subreviewer: ATVA 2025, FASE 2026, HSCC/ICCPS 2026.