Computation Tree Logic Guided Program Repair
Yu Liu, Yahui Song, Martin Mirchev, Abhik Roychoudhury
TL;DR
This work presents CTLexpert, a Datalog-based framework for automatically repairing infinite-state programs to satisfy Computation Tree Logic (CTL) specifications, addressing the limitations of test-based repair by considering all counterexamples symbolically. It extends Symbolic Execution of Datalog (SEDL) to support stratified negation and introduces a novel loop summarization using guarded omega-regular expressions to handle both terminating and non-terminating behaviours, enabling precise CTL analysis. The approach translates CTL properties into stratified Datalog and converts CFGs into guarded omega-REs, which are then encoded as Datalog programs whose results are checked with SEDL; when properties fail, patches are derived by solving symbolic constraints and mapped back to source-level edits. Empirical results show CTLexpert achieves higher verification accuracy than baselines and can repair all detected CTL violations in tested benchmarks, offering a practical, scalable solution for CTL-guided program repair with robust loop handling. The work advances the state of the art by combining CTL-aware Datalog repair, loop summarization, and ASP-assisted negation, providing a path toward reliable automatic repair for complex software systems.
Abstract
Temporal logics like Computation Tree Logic (CTL) have been widely used as expressive formalisms to capture rich behavioral 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 realize this vision, we propose a repair 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. Previous research proposed a generic repair mechanism for Datalog-based analysis in the form of Symbolic Execution of Datalog (SEDL). However, SEDL only supports positive Datalog, which is insufficient for expressing CTL properties. Thus, we extended SEDL to make it applicable to stratified Datalog. Moreover, liveness property violations involve infinite computations, which we handle via a novel loop summarization. Our approach achieves analysis accuracy of 56.6% on a small-scale benchmark and 88.5% on a real-world benchmark, outperforming the best baseline performances of 27.7% and 76.9%. Our approach repairs all detected bugs, which is not achieved by existing tools.