Please note: This distinguished lecture will take place in DC 1302 and online.
Nikolaj Bjørner
Partner Researcher, Microsoft Research
Coding agents are transforming software engineering, accelerating the development of entire systems while creating new opportunities for rigorous engineering. The Research in Software Engineering (RiSE) group at Microsoft Research is embracing this opportunity by integrating formal tools both into agents’ development workflows and into the verification of agents themselves. With proof tools such as F* and Verus, coding agents formalize and audit code changes and prove properties of fundamental algorithms and production code at scale.
These advances bring the aspiration of program verification as a solved problem closer, while sharpening a central challenge: ensuring that specifications capture appropriate intent and that automated reasoning tools, such as Z3, can be driven effectively to produce strong guarantees. To harness agents, GitHub Agentic Workflows bring continuous AI to developers’ fingertips, opening the prospect of a 1000x developer. Complementing verification of the code agents produce, Agent Verification systems apply techniques grounded in formal methods to diagnose agent runtimes and enforce guardrails on their behavior.
Bio: Nikolaj Bjørner’s main line of work is around the state-of-the-art SMT constraint solver Z3. Z3 is used for program verification and test case generation among several applications. The work on Z3 has received several awards. At Azure Networking, Z3 is used for verifying firewall access restrictions, data-center routing and wide area networks. He is a 2021 ACM Fellow. He is currently a partner research manager at Microsoft Research, Redmond.
To attend this distinguished lecture in person, please go to DC 1302. You can also attend virtually on Zoom.