The RiSE of Agentic Software Engineering

Abstract: Coding agents are transforming the craft of software engineering. While demonstrating initial promise a year ago, current coding agents are now capable of coding entire systems end-to-end. Furthermore, systems based on capabilities of last year’s AI systems are increasingly made obsolete. This new reality presents incredible opportunities for advancing engineering with coding agents. The Research in Software Engineering, RiSE, group at Microsoft Research, is currently pursuing agents for research software engineering through: Agent Verification systems that address what it means to diagnose and guard-rail agent runtimes based on techniques grounded in formal methods;

GitHub Agentic Workflows that bring continuous AI to the fingertips of developers towards unlocking 1000x productivity gains; DeepProof employing coding agents to formalize and rigorously prove production code and fundamental computer science algorithms at scale; and DeepTest, which integrates specifications for coding agents to produce comprehensive unit tests. Venturing into autonomous coding agents, the Research Software Engineering system, Comet-H, scales coding agents to co-develop new theory and research software. We showcase a use of Comet-H using the a3-python system. It is a new extended static checker for python that was entirely developed by coding agents. It is based on a novel use of polynomial barrier certificates.

Bio: Nikolaj’s main line of work is around the state-of-the-art SMT constraint solver Z3. Z3 was developed with Leonardo de Moura, Lev Nachmanson and Christoph Wintersteiger. Z3 is used for program verification, test case generation among several applications. The work around Z3 has received several awards. Karthick Jayaraman and Nikolaj created the SecGuru tool that is used to validate firewalls and routing configurations for Microsoft Azure. He was named a 2021 ACM Fellow. He is currently a partner research manager at Microsoft Research, Redmond.