Static Abstract Execution from Programs to Models

Speaker

A/Prof. Yulei Sui, UNSW

Abstract

Static analysis has long served as an important basis for program reasoning and verification, enabling the extraction and interpretation of abstract representations of software systems. This talk explores how the principles of static analysis, as developed in our SVF framework, can be extended beyond traditional code analysis to areas such as abstract execution of AI models. As part of this ongoing effort, we are developing the ACT tool, which applies static reasoning to the analysis and verification of neural networks. It builds on the shared foundations between program analysis and neural network verification, both grounded in abstraction and symbolic reasoning over large input spaces. Our early findings indicate that static reasoning techniques provide useful insights for improving the reliability and robustness of modern AI systems.

Bio

Yulei Sui is an Associate Professor at UNSW. His research focuses on software analysis and verification, with an emphasis on developing open-source frameworks for static analysis to improve the reliability and quality of software systems. He also studies the intersection of large language models and software verification. His work has been published in conferences and journals in program analysis and software engineering, and has received recognition through paper awards at ICSE, FSE, OOPSLA, SAS, and CGO. His research has been supported by an ARC Future Fellowship, ARC Discovery Projects, a JSPS Fellowship, and industry funding from Google and Amazon.