Home

Abhishek Kr Singh

Assistant Professor SERC @ IIIT Hyderabad.
Email: abhishek.uor@gmail.com LinkedIn DBLP GoogleScholar ORCID Scopus

I am an Assistant Professor in the Software Engineering Research Centre (SERC) at IIIT Hyderabad, focusing broadly on Formal Methods, Programming Languages, Software Engineering, and Trustworthy AI. I earned my PhD in Computer Science from TIFR Mumbai, working under the esteemed supervision of Prof. Raja Natarajan in the area of Interactive Theorem Proving and Formalized Maths.

I spent two incredible years as a postdoctoral researcher at the Tel Aviv University in Israel woking with Prof. Ori Lahav in the area of semantics of Shared Memory Concurrency and Weak Memory Models. Following that, I took on the role of Senior Research Fellow in the Programing Language and Software Engineering (PLSE) Lab of School of Computing at the National University of Singapore, hosted by Prof. Abhik Roychoudhury.

Research Interests

I primarily work in areas of Formal Methods, Programming Languages, Software Engineering, and Trustworthy AI. My current research efforts are aimed at establishing a formal foundation for Trustworthy Autonomy in Software Development. Through my research, I strive to contribute to a future where technology enhances safety and security in autonomous applications.

News: I am seeking highly motivated students (BTech, MTech, and PhD) to join my research group in any one of the following ongoing projects. If you are a current student at IIIT Hyderabad and interested in exploring any of these topics feel free to contact me!

Contact Info:

Office: 511, Software Engineering Research Center (5th Floor),

Himalaya Block-D, IIIT Hyderabad Campus, Gachibowli, Hyderabad-500032.

Email: abhishek.singh@iiit.ac.in

Current Projects

Trustworthy Automated Programming

The rise of generative AI and large language models has revolutionized the way we approach software development. These technologies allow developers to articulate their desired functionality in natural language, which AI can then interpret to generate code. However, this process is fraught with challenges due to inherent ambiguities in natural language.

Key Challenges

Ambiguity in Natural Languages: The intent behind a developer's description can be misinterpreted by AI, leading to code that may not align with the user's true goals.
Functional Correctness: Ensuring that AI-generated code adheres to specific functional guarantees without human oversight remains complex.

Project Objectives

To create frameworks that bridge the gap between ambiguous natural language descriptions and rigorous formal specifications.
To incorporate trust and reliability into the software development lifecycle by formalizing programmer intent and verifying AI-generated outputs.

Trustworthy Concurrency

In today’s AI-driven world, parallel computing has become even more crucial due to the heightened stress on computational resources. However, parallel programming presents formidable challenges due to the unintuitive nature of the weak memory models underlying most modern computer architectures (such as x86 TSO, POWER, ARM, and RISC-V) and programming languages (like C11 and RC11). Despite extensive research in concurrency semantics, many programmers continue to struggle with reasoning about the correctness of their concurrent code.

Research Focus

To enhance the trustworthiness of parallel programs, we aim to develop new trust ensuring mechanisms, which are mostly automated and derived from a mindful combination of established formal method techniques such as automated theorem proving, model checking, testing, and fuzzing.

Integrating ML into Theorem Proving

Decades of advancements in Theorem Proving using Proof Assistants and related tools have led to the creation of high-assurance software, including notable examples like CompCert, SeL4, and CakeML. Despite these successes, the formalization approach to software development remains outside the mainstream, primarily due to the challenges and costs associated with human involvement in writing and maintaining verified specifications.

Research Focus

This project aims to leverage machine learning techniques to enhance the theorem proving experience. Specific areas of exploration include:

Proof Search and Tactic Generation: Improving the efficiency of proof searches through machine learning-driven techniques and automating tactics generation during the proof completion process.
Hypothesis and Intermediate Lemma Predictions: Employing ML to generate hypotheses and intermediate lemmas that can facilitate theorem proving.

Professional Service

I am always eager to contribute to reviewing conference and journal papers in Formal Methods, Programming Languages, and Software Engineering. I welcome such review requests and look forward to collaborating with you!

Artifact Evaluation (PC): POPL 2025, PLDI 2025, OOPLSLA 2025, CAV 2025, TACAS 2025, POPL 2024, PLDI 2024, OOPLSA 2024, ICFP 2024, TACAS 2024, ICFP 2023.

Reviewing (PC / External): SRC@SPLASH 2024 (PC), iFM 2024 (PC), ICALP 2024, Journal of Automated Reasoning (JAR 2022), SETTA 2017, SETTA 2016.

Publications

Double Auctions: Formalization and Automated Checkers
Mohit Garg, Raja Natarajan, Suneel Sarswat, Abhishek Singh.
(under review) [arxiv]

Assured Automatic Programming via Large Language Models
Martin Mirchev, Andreea Costea, Abhishek Singh, Abhik Roychoudhury.
(under review) [arxiv]

Decidable Verification under Localized Release-Acquire Concurrency
Abhishek Singh, Ori Lahav.
TACAS 2024 [paper][extended][talk]

An Operational Approach to Library Abstraction under Relaxed Memory Concurrency
Abhishek Singh, Ori Lahav.
POPL 2023 [paper][extended][talk]

Verified Double Sided Auctions for Financial Markets
Raja Natarajan, Suneel Sarswat, Abhishek Singh.
ITP 2021 [paper]

Formally Verified Trades in Financial Markets
Suneel Sarswat, Abhishek Singh.
ICFEM 2020 [paper]

A Constructive Formalization of the Weak Perfect Graph Theorem
Abhishek Singh, Raja Natarajan.
CPP 2020 [paper] [talk]

Towards a constructive formalization of Perfect Graph Theorems
Abhishek Singh, Raja Natarajan.
ICLA 2019 [paper]

Formalization of some central theorems in combinatorics of finite sets
Abhishek Singh.
LPAR 2017 (In IWIL Workshop and LPAR Short Presentations) [paper]

Separation Logic to Meliorate Software Testing and Validation
Abhishek Singh, Raja Natarajan.
Trends in Software Testing 2016 [Book Chapter]

A High Performance Modified SPIHT for Scalable Image Compression
Bibhuprasad Mohanty, Abhishek Singh, Sudipta Mahapatra.
IJIP 2011 (International Journal of Image Processing) [paper]

Technical Reports

Formalizing Finite Set Combinatorics in Type Theory.
PhD Thesis, TIFR Mumbai, 2020. [pdf][Shodhganga Link]

Interactive Theorem Proving in Coq and the Curry-Howard Isomorphism.
Reading Project, TIFR Mumbai, 2015. [pdf]

Wavelet Based Embedded Coding for Images.
MTech Thesis, IIT Kharagpur, 2009. [pdf]

Page updated

Google Sites

Report abuse