Talk at InnovFest
Published:
Abhik Roychoudhury gives plenary speech at NUS Research Institute InnovFest Suzhou 2025.
Posts by Collection
news
projects
publications
Agentic Concolic Execution
Published in IEEE Symposium on Security and Privacy, 2026
Concolic execution is a practical test generation technique that explores execution paths by coupling concrete execution with symbolic reasoning. It runs programs on given inputs while capturing symbolic path representations, then mutates and solves these constraints to generate new test inputs for alternative paths. This approach has several fundamental challenges, such as (C1) the inherent complexity of symbolically modeling diverse programming language constructs and environmental interactions, and (C2) the scalability issues of constraint solvers when handling large, complex formulas. In this work, we investigate whether LLM agents can help address these longstanding challenges in test generation. We propose a novel workflow which we call agentic concolic execution. Using an LLM agent for symbolization, our approach is language-agnostic and can handle environmental constraints without additional manual modeling effort. To ease pressure on the constraint solver, we allow an LLM agent to summarize and even reason about constraints directly in natural language. In a significant evaluation of 12 real-world subjects, our research prototype ConcoLLMic attains significantly higher code coverage (115%-233% higher) than state-of-the-art symbolic executors like KLEE that have been painstakingly hand-crafted over many years, and identifies 11 new vulnerabilities. Our results show that multi-step planning and tool integration enable agents to effectively mitigate reliability issues inherent in LLM-based analysis and even reason symbolically about code.
Agentic Verification of Software Systems
Published in ACM International Conference on Foundations of Software Engineering, 2026
Automatically generated code is gaining traction recently, owing to the prevalence of Large Language Models (LLMs). Further, the AlphaProof initiative has demonstrated the possibility of using AI for general mathematical reasoning. Reasoning about computer programs (software) can be accomplished via general mathematical reasoning; however, it tends to be more structured and richer in contexts. This forms an attractive proposition, since then AI agents can be used to reason about voluminous code that gets generated by AI. In this work, we present a first LLM agent, AutoRocq, for conducting program verification. Unlike past works, which rely on extensive training of LLMs on proof examples, our agent learns on-the-fly and improves the proof via an iterative refinement loop. The iterative improvement of the proof is achieved by the proof agent communicating with the Rocq (formerly Coq) theorem prover to get additional context and feedback. The final result of the iteration is a proof derivation checked by the Rocq theorem prover. In this way, our proof construction involves autonomous collaboration between the proof agent and the theorem prover. This autonomy facilitates the search for proofs and decision-making in deciding on the structure of the proof tree. Experimental evaluation on SV-COMP benchmarks and on Linux kernel modules shows promising efficacy in achieving automated program verification. As automation in code generation becomes more widespread, we posit that our proof agent can be potentially integrated with AI coding agents to achieve a generate and validate loop, thus moving closer to the vision of trusted automatic programming.
talks
Abhik Roychoudhury – Agentic AI for Software
Published:
View the presentation slides and the talk.
vacancies
PhD Positions
Published:
We have several PhD positions available to work on exciting topics as part of the AI for Program Reasoning program. These positions start in August 2026 and are based at NUS.
Research Fellow Positions
Published:
We have a large number of postdoctoral Research Fellow positions available to work on exciting topics as part of the AI for Program Reasoning program. Start dates throughout 2026 and 2027.
Program Manager
Published:
We are looking for a senior Postdoctoral Research Fellow to assume the exciting role of Program Manager for the AI for Program Reasoning project. This is a scientific role, but with significant leadership duties.
Research Associate Positions
Published:
We have several Research Associate positions available to work on exciting topics as part of the AI for Program Reasoning program. These positions require at least a Master’s degree. Start dates throughout 2026 and 2027.