Overview
Software bugs and security vulnerabilities pose critical threats to systems our society depends on, leading to economic losses, privacy breaches, accidents, and hindered scientific progress. With the advent of Large Language Models (LLMs), an increasing amount of code is generated automatically by autonomous coding agents. However, this heightened productivity comes with amplified risks — AI can generate code that introduces or propagates security vulnerabilities. As AI-driven code generation outpaces program reasoning approaches, conventional techniques become prohibitively slow and expensive to support fast-evolving systems. For instance, proving the correctness of the seL4 microkernel required 200,000 lines of manual specifications and 20 person-years of PhD-level effort. We need cost-effective automated program reasoning solutions.
Goal
This research project aims to design novel AI agent techniques for cost-effective automatic program reasoning. This project targets both legacy systems and future AI-assisted software, where AI-generated code is integrated into existing systems. By developing approaches that advance agentic program analysis and proof with augmented code LLMs, this project aims to establish versatile toolkits to reason about complex software systems, such as components in kernels, network and consensus protocols, and multilingual codebases.
Translation
Beyond software engineering, we aim to develop novel AI agent architectures designed for structured reasoning that are applicable to other scientific fields. We envision translation of our agentic reasoning approach into various aspects, such as one-health response, smart cities, and medical devices.
News
-
October 15, 2025
Prof. Abhik Roychoudhury gives plenary speech at NUS Research Institute InnovFest Suzhou 2025.
-
October 03, 2025
Prof. Abhik Roychoudhury speaks on trust in AI agents at IVADO on LLM agents.
-
October 02, 2025
Our project has been funded under the NRF AI for Science call 2025.