Menu
Home
DBLP
Google Scholar
LinkedIn
GitHub
ORCID
Projects
DIFFY
VAJRA
TILER
Resources
CV

Divyesh Unadkat

alt text 

Senior Staff R & D Engineer, Synopsys Inc., Hyderabad

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

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

About

Divyesh Unadkat is a Senior Staff R & D Engineer at Synopsys Inc., Hyderabad. Previously, he was affiliated as a Scientist and Senior Software Engineer with the Foundations of Computing Group, TCS Research, Tata Research Development & Design Centre (TRDDC), Pune.

Divyesh is passionate about research and development challenges in the area of Artificial Intelligence, specifically in the sub-areas of SW/HW Verification, SAT & SMT Solving, Automated Theorem Proving, Data/Control-flow Analysis, Compilers, and Applied Machine Learning.

Divyesh has completed his Ph.D. studies 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). Divyesh has received his Bachelor of Engineering degree in Computer Engineering from Dharmsinh Desai University (DDU).

During his leisure time, Divyesh loves throwing a ball (table tennis, volleyball, football, cricket), stretching his physical limits (exercise, yoga, pranayam, brisk walks), playing with fire & ice; sugar & spice; flour & rice (resulting in nice meals and exotic delicacies), indulging in art forms (suspense & thriller novels, rock & pop music, Hollywood action & romcom movies), exploring the locale (trekking, nature's trail, site seeing, roaming in malls), adding creativity even to day-to-day mundane things and calling up friends and family.

A brief cv.

Experience

Education

  • Degree: Doctor of Philosophy (Ph.D.)
    Thesis: Techniques for Precise and Scalable Verification of Array Programs
    Area: Formal Method and Software Verification
    Lab: Centre for Formal Design and Verification of Software (CFDVS)
    Department: Computer Science and Engineering (CSE)
    Institute: Indian Institute of Technology Bombay (IITB), Mumbai, Maharashtra
    Year: 2015-2022

    Courses Taken
    Formal Specification and Verification of Programs (CS 615)
    Special Topics in Automata and Logics (CS 713)
    Formal Models for Concurrent and Asynchronous Systems (CS 735)
    R&D Project - Abstract Interpretation (CS 691)
    Program Analysis (CS 618)
    Introduction to Computational Complexity (CS 721)
    Applied Algorithms (CS 602)
    Research Seminar (CSS 801)
    Communication Skills (HS 791, CS 792)

  • Degree: Bachelor of Engineering (B.E.)
    Department: Computer Engineering (CE)
    Institute: Dharmsinh Desai University (DDU), Nadiad, Gujarat
    Year: 2006-2010

    Courses Taken
    Software Engineering
    Design of Data Structures and Algorithms
    Computer Programming in C
    Object Oriented Programming and Design - C++
    Core and Advanced Java Technologies
    Discrete Mathematics
    Theory of Automata & Formal Languages
    Language Processors
    Artificial Intelligence
    Database Systems
    Operating Systems
    Linux Operating System & Programming
    Embedded Systems
    Microprocessor Fundamentals and Programming
    Computer Organization
    Advanced Computer Architecture
    Computer Networks
    Advanced Computer Networks

  • Degree: Higher Secondary Education (H.S.E.)
    Department: Science
    Institute: Shree P. V. Modi School, Rajkot, Gujarat
    Year: 2004-2006

  • Degree: Secondary Education (S.S.E.)
    Institute: Saint Mary's School, Gondal, Gujarat
    Year: 1992-2004

Awards & Achievements

  • Spot Award, September 2024, Synopsys Inc. A monetary reward given to high potential employees delivering quality output at pace.

  • Selected for attending the inaugural edition of the ACM Pingla Interactions in Computing, held on 3rd to 6th February 2024, at Infosys Mysore. Only 50 national and international students were selected for participation.

  • SV-COMP win: DIFFY is integrated with VeriAbs and contributed towards winning the ReachSafety category at the Software Verification Competition (SV-COMP) in 2022.

  • SV-COMP win: Tools VAJRA and TILER are a part of VeriAbs and contributed towards winning the ReachSafety category at the Software Verification Competition in (SV-COMP) 2021 and (SV-COMP) 2020.

  • Special Mention acknowledging the SV-Comp win on CSE IITB News page. See the posting dated 22-12-2019.

  • Selected for attending the fifth edition of the Microsoft Academic Research Summit 2020 , held on the 30th and 31st of January 2020 at the BITS Goa campus.

  • 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.

  • Selected for attending Verification Mentoring Workshop (VMW) 2016 and Computer Aided Verification (CAV) 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.

Service

Participation in Conferences and Events

Research Interests

  • Formal Methods & Software Verification

  • Static & Dynamic Program Analysis

  • Applications of Machine Learning to/in Verification

  • AI/ML Compilers

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. Full-Program Induction: A Paradigm Shift in Array Program Verification. Presentation at the Workshop on Research Highlights in Programming Languages, December 2023, IIIT Hyderabad, India. [talk]

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

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

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

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

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

  7. 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]

  8. 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]

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

  10. 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]

  11. 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.

  12. 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.

  13. 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.

  14. 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]

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

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

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