Abstract

Software development is undergoing a profound transformation, with developers increasingly relying on AI assistants and incorporating AI-generated code. These are seismic changes: software systems are evolving faster than ever before, and the core activity of software developers is shifting more and more from writing code to reviewing and validating it.

However, human-scale code review and validation cannot keep up with the speed and volume of AI-driven development. As a result, automated software analysis methods—ranging from fuzzing to symbolic execution to formal verification—are becoming critical safeguards in this AI era. To remain effective, these methods must scale along multiple dimensions: they must handle larger codebases, keep up with increasingly rapid development cycles, operate across a growing diversity of programming languages and system architectures, and infer and reason about higher-level semantic properties.

In this talk, I argue that testing and analysis techniques can themselves take advantage of AI. I will present our recent research efforts in this direction, including our work on designing an agentic concolic executor, an agentic hybrid fuzzer, and an LLM-based technique for inferring the intent of software patches. These systems build on traditional analysis techniques but leverage large language models and agentic AI frameworks to extend their capabilities along the dimensions discussed above. I end the talk by reflecting on the comparative strengths and weaknesses of traditional and AI-based testing and analysis techniques and what this means for building trustworthy software in an era increasingly shaped by AI-generated code.

Keynote at 27th International Symposium on Formal Methods (FM 2026).