Computation Tree Logic Guided Program Repair

Yu Liu

doi:10.1109/TSE.2025.3625772

Return

Computation Tree Logic Guided Program Repair

2025-10-27

DOI：10.1109/TSE.2025.3625772

Original

Original request for help

Save

Abstract

En 中文

Temporal logics like Computation Tree Logic (CTL) have been widely used as expressive formalisms to capture rich behavioural specifications. CTL can express properties such as reachability, termination, invariants and responsiveness, which are difficult to test. This paper suggests a mechanism for the automated repair of infinite-state programs guided by CTL properties. Our produced patches avoid the overfitting issue that occurs in test-suite-guided repair, where the repaired code may not pass tests outside the given test suite. To realise this vision, we propose a novel find-and-fix framework based on Datalog, a widely used domain-specific language for program analysis, which readily supports nested fixed-point semantics of CTL via stratified negation. Specifically, our framework encodes the program and CTL properties into Datalog facts and rules and performs the repair by modifying the facts to pass the analysis rules. In the framework, to achieve both analysis and repair results, we adapt existing techniques – including loop summarisation and Symbolic Execution of Datalog (SEDL) – with key modifications. Our approach achieves analysis accuracy of 56.6% on a CTL verification benchmark and 88.5% on a termination/responsiveness benchmark, surpassing the best baseline performances of 27.7% and 76.9%, respectively. Our approach repairs all detected bugs, which is not achieved by existing tools.

Keywords:

Program analysis and automated repair

datalog

loop summarisation