About Me
I'm a research scholar in the Department of Computer Science & Engineering, IIT Delhi. I work in program analysis and verification of relaxed memory concurrent programs.
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.
I have submitted my dissertation on
Efficient Program Analysis under Relaxed Memory Concurrency for review in February 2023. I completed my synopsis (pre-disseration internal exam) in August 2022.
Resume
Research Statement
Synopsis Presentation
Synopsis Video
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.
In this study, we investigate 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. These weaknesses not only impact their performance but also hinder the generation of effective stress tests. Therefore, 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 peer review)
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.
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.
As a part of this job is was on the organizing committee for the following conferences.
Internships
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
Formal Methods 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
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)
