Modern software is becoming increasingly difficult to secure and reason about as systems grow in complexity, adopt specialized execution environments, and increasingly incorporate AI components. Traditional software analysis provides precise reasoning, but often relies on program knowledge, specifications, or execution environments that are difficult to construct manually. Large Language Models offer complementary capabilities, as they can recover semantic knowledge and generate useful analysis artifacts, but their outputs alone provide limited assurance of correctness. This talk explores how neural (LLMs) and symbolic techniques can work together to overcome these limitations. Across compiler testing, memory safety, trusted execution environments, and emerging AI software ecosystems, LLMs help recover knowledge that is difficult to encode manually, such as testing strategies, memory-management summaries, and lightweight execution environments. Program analysis and symbolic reasoning then use this knowledge to systematically explore program behavior and validate potential issues. This combination enables analyses that would otherwise require substantial manual modeling. Applied to real-world systems, these approaches have uncovered more than 360 previously unknown compiler bugs and memory leaks, as well as security and compliance issues ranging from insecure trust boundaries to license conflicts affecting models with over 100 million downloads. Together, these works demonstrate the potential of combining neural flexibility with symbolic rigor for software assurance.
Speaker Info:
Jieke Shi is a Research Scientist and NRF Postdoctoral Award Recipient at the School of Computing and Information Systems (SCIS), Singapore Management University (SMU), where he also obtained my PhD. He is working with Professor David Lo, an ACM/IEEE/ASE Fellow, as his supervisor.