About Me
I hold a Ph.D. degree from the Indian Institute of Technology Delhi (IITD) on
Program Analysis under Relaxed Memory Concurrency.
My research work can be described by the following keywords: stateless model checking, dynamic and static program analysis, concurrency, weak memory models, sound and optimal analysis, efficient techniques for scalability and performance, as well as effective implementation strategies.
Prior to this I was working at
Jaypee University of Information Technology, Solan H.P. as Assistant Professor in the Department of Computer Science & Engineering.
I completed my masters through an integrated B.Tech-M.Tech in Computer Science from
Jaypee Institute of Information Technology, Noida, U.P.
Resume
CV
Research Statement
Ph.D. Thesis
Ph.D. Defence Video
Future Research Goals.
Scalable program analysis
During my Ph.D., I focused on the development of sound and optimal analysis techniques which are limited in scalability and performance. Moving forward, I aim to create scalable approaches capable of efficiently handling large programs. These techniques may leverage symbolic execution, integrate machine learning, or utilize parallelization, all while ensuring the quality of results remains satisfactory.
Application of program analysis techniques to other programming paradigms
I am interested in exploring the application of program analysis techniques to other programming paradigms, including concurrent data structures, database transactions, distributed systems, and neural networks.
Synthesis under relaxed models
While I have briefly explored program synthesis with my C11 fence synthesis project, I believe there is a vast scope for synthesis under relaxed models that I would like to explore and address. Specifically, there is scope for automated correction of bugs induced by relaxed semantics and for automated transformations that optimize the utilization of relaxed ordering.
|
Member of Vertecs Research Group
VERification, TEsting, Concurrency, Security / Semantics (VERTECS
2) is a research group in the Department of Computer Science and Engineering at IIT Delhi. We have members working in the areas of formal verification, concurrency, programming languages and security. The group wepage can be found
here.
The webpage for the group has been designed by me.
Currently Working On
Automated Bug Detection and Repair in C11 Programs: Insights and Experiences (under peer review)
The C / C++ 2011 standard, which introduced the C11 weak memory model, offers syntactic constructs to specify a range of ordering guarantees for development of efficient weak memory concurrent programs. However, the complexity of the model poses challenges and can lead to programming bugs. To fully leverage the potential of the C11 model, robust development support is crucial.
We present the first study that investigates the existing development support for C11 programs, focusing specifically on bug detection and automated repair. We propose a novel set of stress tests for C11 generated by utilizing automated repair techniques. We explore various bug detection techniques for C11 and assess their performance on these novel stress tests. Through our investigation, we uncover both strengths and weaknesses that were previously unreported. Additionally, we identify weaknesses in the existing automated code repair techniques that not only impact their performance but also hinder the generation of effective stress tests. Finally, building upon our investigative findings, we propose improvements to enhance the automated repair capabilities under C11 .
Optimal Stateless Model Checking based on a Coarse Trace Equivalence (under revise and resubmit for OOPSLA)
Partitioning program executions into equivalence classes is central to efficient stateless model checking of concurrent programs. An equivalence relation drives the partitioning, and prior works have investigated various such relations toward minimizing the set of equivalence classes. This work introduces a novel view-equivalence partitioning relation that relies on the values read by memory accesses. Two program executions are view-equivalent if (i) they have the same set of read memory accesses and (ii) the read memory accesses read the same values. For any input program, view-equivalence is at least as coarse as any existing equivalence relation and, thus, induces the least number of equivalence classes. This work also proposes a stateless model checker based on view-equivalence, called ViEqui, that is sound, complete, and optimal under view-equivalence. ViEqui is implemented for C/C++ input programs over the Nidhugg tool. We test its correctness over 16000+ litmus tests and compare its performance against prior stateless model checkers on challenging benchmarks. Our experiments reveal that ViEqui performs over 20x faster in ∼18% of tests and times out in significantly lesser tests than other existing techniques.
Optimal Stateless Model Checking based on a Coarse Trace Equivalence under RA memory model
Most modern architectures support memory models that are more relaxed than the the sequentially consistent memory model. In this work we propose a stateless model checker based on the coarse view-equivalence relation for the RA relaxed memory model. The RA memory model has gained popularity in recent years as it strikes a good balance between performance and programmability. However, stateless model checking the supported relaxed behaviors based on coarse trace equivalence is non-trivial as RA does not provide much of the ordering that is implicitely provided by sequential consistency.
Lock-aware Optimal Stateless Model Checking based on a Coarse Trace Equivalence
Coarse-grained synchronization mechanisms such as locks are the most popular techniques for providing synchronization in concurrent programs. The coarse-grained locks introduce lock acquisition events whose interleaving order may determine which thread acquires the lock-object and accordingly which events are enabled. Thus, various orders of interleaving of lock acquisition events may lead to different equivalence classes. Since equivalence classes are not known to SMCs a-priori, they must explore various possible orders of lock acquisitions for completeness. This work extends the ViEqui technique by considering lock acquisition and unlock or release lock events, along with read and write events, and performs analysis observing consistent coarse-grained synchronization. As an optimization against considering all feasible lock acquisition orders, \laviequi technique pivots on recognizing the feasibility of the reads-from relation. Essentially, the technique seeks an order of lock acquisitions that permit the required reads-from relation.
|
Publications
Work Experience
Jaypee University of Information Technology, Solan H.P.
Assistant Professor
01 July 2013 - 30 June 2016
The job included teaching undergrad and postgrad courses with laboratory components along with research in computer science and its applications. At JUIT I started the technical club of the CSE department called "Enkindle" and conducted its first technical fest in 2015.
Other designations at JUIT
- Training and Placement CSE head
- Faculty in-charge of CSE technical club Enkindle
As a part of this job is was on the organizing committee for the following conferences.
Indian Institute of Technology
Teaching Assistant
01 July 2013 - 30 June 2016
Internships
Early-doc Fellowship
01 August - 31 October 2023
Indian Institute of Technology Delhi
Fellowship to support ongoing research projects at IITD under the supervision of Subodh Sharma, Department of Computer Science and Engineering, IITD.
Japan-Asia Youth Exchange Program in Science (SAKURA)
25 June - 15 July 2017
University of Tokyo
SAKURA is a program for enhancing exchanges between Asia and Japan aiming at future close collaboration of industry-academia-government by facilitating short-term visits to Japan. You can read about
my experience.
Bharti Airtel Ltd. (Enterprise services North & East)
30 May - 08 July 2011
Gurgaon
Summer Internship/Industrial Training that involved assistance on installing routers.
Technical Presentations/Talks
Workshop on Research Highlights in Programming Languages (Co-located withFSTTCS 2023)December 2023
Title:
Optimal Stateless Model Checking based on View-equivalence
Presentation
21 st International Symposium on Automated Technology for Verification and Analysis (ATVA)September 2023
Title:
Fence Synthesis Under the C11 Memory Model
Presentation
Formal Methods India Update Meeting 2023July 2023
Title:
Optimal Stateless Model Checking based on View-equivalence
Presentation
Software Engineering Research in India (SERI) 2023 Update MeetingJune 2023
Title:
Fence Synthesis under the C11 Memory Model
Presentation
20th International Symposium on Automated Technology for Verification and Analysis (ATVA)October 2022
Title:
Fence Synthesis under the C11 Memory Model
Presentation
Video
12th Annual IEEE India Conference (INDICON)December 2015
Title:
A novel approach for bug localization for Exception Handling and Multithreading through mutation
Workshops
The Third Indian SAT+SMT School06-08 December 2018
IIIT Hyderabad
The theme of the school was encodings in the solvers.
The Second Indian SAT+SMT School06-08 December 2017
Infosys-Mysore
The theme of the school was quantifiers in solvers with tutorials on Quantified Boolean Formulas, Quantifiers in SMT solvers and Quantified invariants in verification tools.
I was member of the support organizers for the school and had created the official school webpage.
Winter School in Software Engineering (WSSE)11-16 December 2017
TRDDC-Pune
The school included talks, tutorials and hands-on sessions focused program analysis and verification.
The First Indian SAT+SMT School04-10 December 2016
TIFR-Mumbai
The workshop included a basic course on logic, tutorials on solvers by eminent scientists and developers from around the world, and latest research and applications centered around these solvers.
Projects
Software Source-Code Analysis Related to Plagiarism Dispute
for the Hon'ble Delhi High Court
We present a comprehensive report in terms of the order passed by the Hon'ble Delhi High Court. The two disputing parties both implemented their backend processing in Java and their frontend processing in CSS and Javascript. We analyzed the source-codes as a pair-wise comparison between files from the two software, using the tools (i) MOSS, (ii) SIM, and (iii) ScanCode.
Webpage design for Vertecs Research Group
Vertecs is a research group in the Department of Computer Science and Engineering at IIT Delhi.
Webpage design for The Second Indian SAT+SMT School
The Second Indian SAT+SMT School is the second edition of a workshop series on SAT+SMT solvers. This workshop was held in December 2017 at Mysore Infosys Campus, Mysuru, India.
M.Tech. Dissertation
Bug Localization for Exception Handling and Multithreading
Created a prototype tool for a bug localization technique that is based on the hypothesis that a mutant of the source code could be a better approximation of the intended code. The work involved proposal of mutation operators to create mutants to detect buggy lines of code. And testing of proposed mutants for usefulness towards the hypothesis.
B.Tech. Project
Mining mailing list for extracting useful information
Created a query response system that mines developer mailing lists for extracting useful information and possible response to the query and finally producing the best fit match for a user’s query. Used concepts like caching (of frequent responses), stopword elimination and stemming (for refining query), topic modeling (to classify mails in mailer list), sentiment analysis (to marks mails as positive or negative) and ranking mechanism (for ranking the responses).
Courses enrolled at IIT, Delhi
COL765 Introduction to Logic and Functional Programming
COL730 Parallel Programming
COL729 Compiler Optimizations (Sit through)
COL633 Resource Management in Computer Science
COL750 Foundations of Automatic Verification
COL869 Spl. Topics in Concurrency (focus: Concurrent Processes and Bisimulation)
COL871 Spl. Topics in Programming Languages and Compilers (focus: Anstract Interpretation)
COV882 Spl. Module in Software Systems
COL869 Spl. Topics in Concurrency (focus: Petri-nets) (Sit through)
COL869 Spl. Topics in Programming Languages and Compilers (focus: Program Synthesis) (Sit through)
Teaching Assistantship at IIT, Delhi
COL730 Parallel Programming (Jun-Dec '20)
COL106 Data Structures (Jun-Dec '19)
COL380 Introduction to Parallel and Distributed Programming (Jan-May '19)
COL100 Introduction to Computer Science (Jun-Dec '18)
COV889 Special Module in Concurrency (Jan-May '18)
COL380 Introduction to Parallel and Distributed Programming (Jan-May '18)
COL765 Introduction to Logic and Functional Programming (Jul-Dec '17)
COL380 Introduction to Parallel and Distributed Programming (Jan-May '17)
COL729 Compiler Optimizations (Jul-Dec '16)
