Jun 2021 – Jul 2023 · 2 yrs 1 mo · Pune, Maharashtra, India

Jun 2010 – May 2021 · 10 yrs 11 mos · Pune, Maharashtra, India

• Divyesh Unadkat explored software verification techniques that combine Hoare style reasoning with mathematical induction for verifying quantified as well as quantifier-free properties of programs that manipulate arrays. He built tools namely, DIFFY, VAJRA and TILER, that demonstrate the effectiveness and efficacy of the proposed techniques. He has successfully integrated these tools with the TCS verification tool - VERIABS. VERIABS with the help of the tools DIFFY, VAJRA and TILER, outperformed all the other tools in the ReachSafety-Arrays sub-category by a significant margin and won gold medals in 2020, 2021 and 2022. His efforts in this direction have resulted in publications at STTT 2022, CAV 2021, TACAS 2020, SVCOMP 2020 and SAS 2017.
• Previously, he designed novel techniques for scaling model checking for automatic test-data generation and verification of industry strength C programs by learning invariants using dynamic analysis from concrete program traces (using the Daikon tool). He implemented these techniques in TCS Internal tools ScaleM and DIV. Publications in the Ninth Haifa Verification Conference (HVC 2013) and the Sixth International Conference on Software Testing, Verification and Validation (ICST 2013) have come out of this work.
• Prior to that, he worked on the design and development of an automatic test-data generation tool for C programs called AutoGen. The tool generates structural test-cases for various coverage criteria such as MC/DC, Boundary Value, Decision Coverage and so on. It employs a model checker (CBMC) to check assertions in the annotated C source code.

Jan 2015 – Aug 2022 · 7 yrs 7 mos · Mumbai, Maharashtra, India

• Divyesh Unadkat was a Research Scholar in the Computer Science and Engineering (CSE) Dept. at the Indian Institute of Technology Bombay. His research interests include Software Verification, Security & Reliability, Program Analysis, Compilers, Artificial Intelligence and Applied Machine Learning.
• He was affiliated with the Centre for Formal Design and Verification of Software (CFDVS) at IITB where he explores techniques that combine Hoare style reasoning with mathematical induction for verifying quantified as well as quantifier-free properties of programs that manipulate arrays. His efforts in this direction, under the guidance of Prof. Supratik Chakraborty and Prof. Ashutosh Gupta, have resulted in publications at STTT 2022, CAV 2021, TACAS 2020, SVCOMP 2020 and SAS 2017. During his PhD, he has built tools namely, Diffy, VAJRA and TILER, using LLVM 6.0 compiler framework and Z3 smt solver, that demonstrate the effectiveness and efficacy of the proposed techniques. He has successfully integrated his tools DIFFY, VAJRA and TILER with the TCS verification framework VERIABS. In the Software Verification Competition (SV-COMP), VERIABS along with his tools DIFFY, VAJRA and TILER have outperformed all the other tools in the Arrays subcategory by a significant margin and won gold medals in the ReachSafety category in 2020, 2021 and 2022.
• His work got featured on cse webpage at https://www.cse.iitb.ac.in/about/news.php?year=2019&id=545
• Notable Online Presentations:
• FM Update 2021: https://www.youtube.com/watch?v=ATa9eCGLYOM&t=0s
• CAV 2021: https://recorder-v3.slideslive.com/#/share?share=41171&s=d5a2a32c-4e3e-444b-8db2-9a6ced55d6d6
• TACAS 2020: https://www.morressier.com/session/605259628b2e1f00186fe05f
• SERI 2020: https://www.youtube.com/watch?v=fMO2-rgmUBQ
• Indian SAT+SMT School 2020: https://www.youtube.com/watch?v=XvLH9I4tpOk

Dec 2009 – Apr 2010 · 4 mos · Pune, Maharashtra, India

• Various forms of state charts are used to describe the behavior of embedded systems. Harel state charts are widely used to model real time reactive systems using Statemate tool. The state charts need to be verified for detecting erroneous conditions like Non Determinism, Race Conditions and State Reachability. The model checker bundled with Statemate does not scale on large statecharts (~100 states).
• We observed that the sal-bmc model checker scales better when compared to the internal model checker of Statemate.
• To make effective use of the scalable model checker Sal-bmc, I (along with my co-intern) designed and developed a tool that translates state charts to SAL specification. We applied the sal-bmc model checker available in the SAL framework and demonstrated solid performance gains.