Symbolic Execution of Datalog and its Application to Static Analysis Guided Program Repair

This talk introduces a new automated reasoning approach, symbolic execution of Datalog (SEDL). Datalog is a query language based on logic programming, which is used, among other applications, as a domain-specific language for defining program analysers. SEDL executes a Datalog query on a database of symbolic facts to compute dependencies between the input and the output of the query. We propose an efficient approach to implement SEDL on top of an existing Datalog solver using meta-programming.

We apply SEDL to static analysis guided program repair. We represent the buggy program that violates a static analysis property as Datalog facts, while the fixed-point equations of the static analysis are expressed through recursive Datalog rules. Then, the act of repairing the program is seen as modifying the corresponding Datalog facts. We execute SEDL to deduce the necessary alterations of the facts to meet the desired static analysis objectives.

We evaluated SEDL with existing third-party Datalog-based static analysers for detecting null pointer exceptions in Java programs, data leaks in Python notebooks, and four types of security vulnerabilities in Solidity smart contracts. We showed that SEDL-based program repair achieves a comparable or better performance than existing ad-hoc approaches designed to fix these classes of bugs, while also decoupling program analyses logic from program repair. It lays the foundation for developing a modular, general-purpose static program repair system that is able to address a wide range of defects.

Sergey Mechtaev is a Lecturer at University College London and a member of CREST center. Previously, he obtained a PhD degree from the National University of Singapore. His research interests include automated program repair, symbolic execution, and AI-based program analysis. Among other things, he developed Angelix, the first constraint-based program repair system that scaled to real-world programs, and founded program-repair.org, the largest online community of program repair researchers. For his research on automated program repair, he received ACM SIGSOFT Outstanding Dissertation Award in 2019 and ACM SIGSOFT Distinguished Paper Award in 2023. His web page is https://mechtaev.com