The RiSE of Agentic Software Engineering, Dr Nikolaj Bjørner, 02/11/2026, 11:00, Α56

-
Meeting Room A56, Department of Informatics and Telecommunications

Nikolaj Bjørner (Microsoft Research) talk at DIT

Microsoft Research

Title: Talk: The RiSE of Agentic Software Engineering

Monday, 2 November 2026, 11:00, Meeting Room A56

Speaker: Dr Nikolaj Bjørner* Affiliation: Partner Research Manager, Microsoft Research, Redmond Monday, 2 November, 11:00, Meeting Room A56

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, which 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 through the a3-python system, a new extended static checker for Python that was developed entirely by coding agents. It is based on a novel use of polynomial barrier certificates.

*Nikolaj Bjørner's main line of work is around the state-of-the-art SMT constraint solver Z3, developed with Leonardo de Moura, Lev Nachmanson and Christoph Wintersteiger. Z3 is used for program verification and test case generation, among several other applications, and the work around it has received several awards. Karthick Jayaraman and Nikolaj created the SecGuru tool, used to validate firewall and routing configurations for Microsoft Azure. He was named a 2021 ACM Fellow. He is currently a Partner Research Manager at Microsoft Research, Redmond.