Divyesh Unadkat

alt text 

Ph.D. in Software Verification,
Computer Science and Engineering Department,
Indian Institute of Technology Bombay (IITB)

Room No 301, CFDVS Lab, New CC Building, IIT Bombay,
Powai Area, Mumbai - 400076, Maharashtra, India.

Email: firstname [@] cse [DOT] iitb [DOT] ac [DOT] in

About me

Divyesh Unadkat pursued his Ph.D. in Software Verification under the supervision of Prof. Supratik Chakraborty and Prof. Ashutosh Gupta. He was affiliated with the Centre for Formal Design and Verification of Software (CFDVS) at the Indian Institute of Technology Bombay (IITB). He has received his Bachelor of Engineering degree in Computer Engineering from Dharmsinh Desai University (DDU). He is affiliated as a Scientist and Senior Software Engineer with the Foundations of Computing Group, TCS Research, Tata Research Development & Design Centre (TRDDC), Pune.

A brief cv.

Research Interests

  • Formal Methods & Software Verification

  • Static & Dynamic Program Analysis

  • Optimization Techniques for AI/ML Compilers

  • Machine Learning and its applications to Verification

Experience

Recent Publications

  1. Techniques for Precise and Scalable Verification of Array Programs. Divyesh Unadkat. PhD Thesis, IIT Bombay, 2022. [slides]

  2. Full-Program Induction: Verifying Array Programs sans Loop Invariants. Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat. In International Journal on Software Tool for Technology Transfer (STTT) 2022. [arXiv]

  3. Diffy: Inductive Reasoning of Array Programs using Difference Invariants. Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat. In Proceedings of the 33th International Conference on Computer-Aided Verification (CAV) 2021, Los Angeles, USA. [arXiv] [slides] [talk] [short talk]

  4. Verifying Array Manipulating Programs with Full-Program Induction. Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat. In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2020, Dublin, Ireland. [arXiv] [slides] [talk]

  5. VeriAbs: Verification by Abstraction and Test Generation (Competition Contribution). Mohammad Afzal et. al. In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2020, Dublin, Ireland.

  6. Verifying Array Manipulating Programs by Tiling. Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat. In Proceedings of the 24th International Static Analysis Symposium (SAS) 2017, New York, USA. [arXiv] [slides]

Full list of publications.

Presentations

  1. Inductive Reasoning for Precise and Scalable Verification of Array Programs. PhD defence presentation, January 2023, IIT Bombay, India. [slides]

  2. Frontiers of Inductive Reasoning for Arrays. Presentation at the 7th Indian SAT+SMT School, December 2022, IIT Madras, India. [slides] [talk]

  3. Dance of the Dragons: Induction, Difference Computation, and SMT Solving. Presentation at the Formal Methods Update Meeting FMI, July 2022, IIT Delhi, India. [slides]

  4. Difference Invariants for Inductive Verification. Presentation at the 6th Indian SAT+SMT School, December 2021, Online Event, India. [talk]

  5. Exploiting Induction and Difference Computation to Verify Array Programs. Presentation at the Formal Methods Update Meeting FMI, July 2021, Online Event, India. [slides] [talk]

  6. Diffy: Inductive Reasoning of Array Programs using Difference Invariants. Conference presentation (Online) at the 33th International Conference on Computer-Aided Verification (CAV) July 2021, Los Angeles, USA. [slides] [arXiv] [talk] [short talk]

  7. Verifying Array Manipulating Programs with Full-Program Induction. Conference presentation (Online) at the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), March 2021, Luxembourg. [slides] [arXiv] [talk]

  8. The Full-Program Induction Technique. Presentation at the 5th Indian SAT+SMT School, December 2020, (Online Event) Indian Institute of Technology, Hyderabad, India. [talk]

  9. Invited Talk: Verifying Array Manipulating Programs with Full-Program Induction. Invited presentation at the 2nd Software Engineering Research in India (SERI), July 2020, (Online Event) International Institute of Information Technology, Hyderabad, India. [talk]

  10. Technical Poster: Verifying Array Programs with Full-Program Induction. Poster presentation at the 4th Indian SAT+SMT School, December 2019, Indian Institute of Technology Bombay, Mumbai, India.

  11. Executive Poster: Tiling to Verify Array Programs. Poster presentation at the TCS Anvetion Workshop, 2018, IITM Research Park, Indian Institute of Technology Madras, Chennai, India.

  12. Short Talk: Verifying Array Manipulating Programs by Tiling. Short presentation at the 2nd Indian SAT+SMT School, December 2017, Infosys Leadership Institute, Mysore, Karnataka, India.

  13. Verifying Array Manipulating Programs by Tiling. Conference presentation at the 24th International Static Analysis Symposium (SAS), August 2017, New York University, New York, NYC, USA. [slides]

  14. Competition Talk: Verifying Array Manipulating Programs by Tiling. Research and Innovation Symposium in Computing (RISC), April 2017, Indian Institute of Technology Bombay, Mumbai, India.

  15. Competition Talk: Towards Precise Software Verification. Research and Innovation Symposium in Computing (RISC), April 2016, Indian Institute of Technology Bombay, Mumbai, India.

  16. Assertion Checking using Dynamic Inference. Conference presentation at the 9th Haifa Verification Conference (HVC), November 2013, IBM Research, Haifa, Israel.

Awards & Achievements

  • DIFFY is integrated with VeriAbs that participates in the ReachSafety category at the Software Verification Competition (SV-COMP) since 2022.

  • Tools VAJRA and TILER are a part of VeriAbs that won a Gold medal in the ReachSafety category at the Software Verification Competition (SV-COMP) 2020.

  • Won the Honorable Mention award in Sprint Thesis Talks Competition at Research and Innovation Symposium in Computing (RISC) 2017.

  • Won the Best Talk award in Sprint Thesis Talks Competition at Research and Innovation Symposium in Computing (RISC) 2016.

  • Awarded the "Eklavya Gold Medal" for securing the highest aggregate at the end of four semesters among all B.E students in Computer Engineering discipline of 2010 batch, Dharmsinh Desai University, Nadiad.

Community Service

Event Participation