Machine learning, in particular Large Language Models, has shown great promise at automating several aspects of programming and software development such as coding, testing, integration, static analysis, verification etc. in recent years. In this project, we leverage and extend large language models with ideas grounded in programming languages and correctness to develop trusted AI agents for all aspects of programming for reliable software development..

Current work explores various directions, user-intent formalization (high-level deck) through (a) neural test (oracle) generation to find functional bugs in TOGA, (b) test-driven interactive intent-formalization for improving accuracy and explainability of code generation in TiCoder, (c) generating program specifications from natural language as in nl2postcond, and (d) instantiating these ideas for security-critical domains such as verified parser generation from RFC descriptions in 3DGen. We explore program proof automation using neural techniques including (a) improving LLMs ability to generate correct loop invariants by neurally ranking LLM-generated loop invariants in iRank, and (b) creating large-scale dataset and fine-tuned models for proof automation for proof-oriented programming (PoPAI) in languages such as F*. Other works include fine-tuning large language models on test execution data to predict runtime faults for generated code in CodeRanker, and improving search-based test generation with LLMs in CodaMOSA.