CTL* Verification and Synthesis using Existential Horn Clauses

Mishel Carelli; Orna Grumberg

arxiv: 2408.11502 · v1 · submitted 2024-08-21 · 💻 cs.LO

CTL* Verification and Synthesis using Existential Horn Clauses

Mishel Carelli , Orna Grumberg This is my paper

Pith reviewed 2026-05-23 21:29 UTC · model grok-4.3

classification 💻 cs.LO

keywords CTL*verificationsynthesisexistential Horn clausesinfinite-state programstemporal logicreactive systemsE-HSF

0 comments

The pith

A translation turns CTL* verification and synthesis for infinite-state programs into satisfiability of existential Horn clauses.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a translation system Trans that takes an infinite-state reactive program P and a CTL* formula φ and produces a set of existential Horn clauses. The set is satisfiable precisely when P satisfies φ. A companion synthesis procedure fills holes in conditions and assignments so the completed program meets the given CTL* specification. Both procedures are shown to be sound and relatively complete with respect to an underlying E-HSF solver that handles existential quantification and well-foundedness constraints. The reduction therefore lets existing EHC technology decide CTL* properties and construct programs that obey them.

Core claim

Verification of whether program P satisfies CTL* formula φ reduces exactly to satisfiability of the EHC set produced by Trans; synthesis reduces to finding values for the holes that make the corresponding EHC set satisfiable. Both algorithms are sound (satisfiable EHCs imply the program meets the spec) and relatively complete (if the program meets the spec, the EHCs are satisfiable).

What carries the argument

The translation system Trans, which converts CTL* formulas together with the program transition relation into existential Horn clauses that encode both the specification and the required well-foundedness conditions.

If this is right

Any CTL* property on an infinite-state program can be checked by solving the corresponding EHC instance.
Programs with holes in guards and updates can be completed automatically so that the result satisfies a given CTL* formula.
Because CTL* contains both LTL and CTL, the same machinery covers verification and synthesis for those sublogics.
Relative completeness guarantees that every program satisfying the specification will be found if the E-HSF solver is complete on the generated clauses.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same reduction pattern could be applied to other branching-time or hybrid logics once their semantics are expressed as well-foundedness constraints.
Practical performance will depend on how efficiently current E-HSF implementations handle the particular clause shapes produced by Trans.
The method offers a uniform route from specification to implementation that could be composed with existing program-repair or counterexample-guided synthesis loops.

Load-bearing premise

The mapping from CTL* formulas and program semantics to existential Horn clauses preserves satisfiability in both directions.

What would settle it

A concrete infinite-state program and CTL* formula for which the generated EHC set is satisfiable yet the program violates the formula, or unsatisfiable yet the program satisfies the formula.

Figures

Figures reproduced from arXiv: 2408.11502 by Mishel Carelli, Orna Grumberg.

**Figure 1.** Figure 1: Robots program R Suppose we are given a system with three robots placed on rational points of a two-dimensional plane. A user makes an ongoing interaction with the system by sending commands. The system processes the commands and moves the robots accordingly. We wish to verify two properties. The first property states that the three robots are never located in the same position at the same time. The secon… view at source ↗

**Figure 2.** Figure 2: Synthesizing bank-client interaction The synthesized condition on line lc assures that the client has enough money to pay for his request and for the cost of transaction, $0.1, so that the bank would not lose its profit. On lines la1 and la2 of BS the bank collects $0.1 from the client’s account. Additionally, on line la2 the bank collects 6% of req, thus pro is at least 6% of exp and it never decreases. T… view at source ↗

read the original abstract

This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to ${CTL}^*$ specifications, based on translation to Existential Horn Clauses (EHCs). $CTL^*$ is a powerful temporal logic, which subsumes the temporal logics LTL and CTL, both widely used in specification, verification, and synthesis of complex systems. EHCs with its solver E-HSF, is an extension of Constrained Horn Clauses, which includes existential quantification as well as the power of handling well-foundedness. We develop the translation system \textit{Trans}, which given a verification problem consisting of a program $P$ and a specification $\phi$, builds a set of EHCs which is satisfiable iff $P$ satisfies $\phi$. We also develop a synthesis algorithm that given a program with holes in conditions and assignments, fills the holes so that the synthesized program satisfies the given $CTL^*$ specification. We prove that our verification and synthesis algorithms are both sound and relative complete. Finally, we present case studies to demonstrate the applicability of our algorithms for $CTL^*$ verification and synthesis.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper reduces CTL* verification and synthesis to existential Horn clause satisfiability with claimed soundness and relative completeness.

read the letter

The main takeaway is that this paper presents a translation system Trans turning a program plus CTL* specification into existential Horn clauses that are satisfiable exactly when the program meets the spec, plus a synthesis procedure for filling holes in conditions and assignments, with soundness and relative completeness proved for both. The reduction itself looks new relative to prior constrained Horn clause work and CTL* model checking. Extending the approach to full CTL* (which covers both linear and branching properties) and to synthesis is a genuine step forward, since EHCs can express existential quantification and well-foundedness needed for infinite-state reactive systems. The positioning against existing techniques is clear and the claims are stated directly. The soft spots are limited. The abstract gives no example translation or proof sketch, so it is not possible to inspect how CTL* operators or well-foundedness constraints are encoded without the full text; that makes initial assessment slower but does not indicate a flaw. The case studies are referenced without performance numbers or example sizes, which is a minor presentational gap. The central argument appears to hold on the description given, with no internal inconsistency or circularity. This paper is aimed at researchers in automated verification who already work with Horn-clause solvers or temporal logics for reactive systems. A reader following constraint-based model checking would find the most direct value. It deserves a serious referee because the reduction targets an expressive logic and includes both verification and synthesis. I would recommend sending it out for peer review rather than desk rejection.

Referee Report

1 major / 0 minor

Summary. The paper proposes a translation system Trans that, given an infinite-state reactive program P and a CTL* specification ϕ, produces a set of Existential Horn Clauses (EHCs) satisfiable if and only if P satisfies ϕ. It also presents a synthesis algorithm that fills holes in conditions and assignments so the resulting program satisfies a given CTL* specification. Both the verification and synthesis procedures are claimed to be sound and relatively complete, with case studies demonstrating applicability.

Significance. If the translation preserves satisfiability exactly and the soundness/relative-completeness arguments hold, the work would extend constrained-Horn-clause techniques to the full expressive power of CTL* (which subsumes LTL and CTL) while leveraging the existential-quantification and well-foundedness capabilities of E-HSF solvers. This could be a useful addition to the toolkit for reactive-program verification and synthesis.

major comments (1)

[Abstract] Abstract: the manuscript asserts that 'We prove that our verification and synthesis algorithms are both sound and relative complete,' yet supplies no derivation details, no example translations of CTL* formulas or program semantics, and no discussion of how well-foundedness constraints or existential quantification are encoded. Because these proofs are the load-bearing justification for the central claim that the EHC set is satisfiable exactly when the program satisfies the specification, their absence prevents verification of correctness.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their review. The manuscript contains the requested details on the translation, proofs, and encodings in the body of the paper; we address the concern below.

read point-by-point responses

Referee: [Abstract] Abstract: the manuscript asserts that 'We prove that our verification and synthesis algorithms are both sound and relative complete,' yet supplies no derivation details, no example translations of CTL* formulas or program semantics, and no discussion of how well-foundedness constraints or existential quantification are encoded. Because these proofs are the load-bearing justification for the central claim that the EHC set is satisfiable exactly when the program satisfies the specification, their absence prevents verification of correctness.

Authors: We respectfully disagree that these elements are absent from the manuscript. The translation system Trans is defined in Section 3, which includes concrete examples of translating CTL* formulas (e.g., combinations of path quantifiers A/E with temporal operators G/F/U) and the operational semantics of reactive programs into EHCs. The proofs of soundness and relative completeness appear as Theorems 1 and 2 in Sections 4 and 5, respectively; these arguments explicitly address the preservation of satisfiability, including the encoding of well-foundedness constraints (via ranking functions) and existential quantification (via the capabilities of E-HSF). Section 2.2 discusses the relevant features of EHCs, and Section 6 illustrates their use in the case studies. If the referee overlooked these sections, we are happy to expand cross-references or add further examples in a revision. revision: no

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines a translation Trans from a program P and CTL* formula phi to a set of existential Horn clauses, then separately proves that the EHC set is satisfiable exactly when P satisfies phi, along with soundness and relative completeness for both verification and synthesis. No load-bearing step reduces by construction to a fitted parameter, self-citation, or prior ansatz from the same authors. The central claim rests on an explicit, independently stated translation and proof rather than any of the enumerated circular patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The approach rests on the existence of a correct solver for existential Horn clauses that can handle well-foundedness and on the claim that the translation preserves satisfiability exactly. No free parameters or invented entities are introduced in the abstract.

axioms (2)

domain assumption CTL* semantics can be encoded into existential Horn clauses while preserving satisfiability
Invoked when defining the translation system Trans
domain assumption The E-HSF solver decides satisfiability of the generated EHCs correctly
Required for both verification and synthesis algorithms to be sound

pith-pipeline@v0.9.0 · 5725 in / 1405 out tokens · 17491 ms · 2026-05-23T21:29:06.722375+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

26 extracted references · 26 canonical work pages

[1]

Beyene, T.A., Brockschmidt, M., Rybalchenko, A.: CTL+FO veriﬁcation as con- straint solving (2014)

work page 2014
[2]

In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, ACM, pp

Beyene, T.A., Chaudhuri, S., Popeea, C., Rybalchenko, A. : A constraint-based approach to solving games on inﬁnite graphs. In: Jagannatha n, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Prin ciples of Programming Languages, POPL ’14, San Diego, CA, USA, Janu ary 20- 21, 2014. pp. 221–234. ACM (2014). https://doi.org/10.114 5/25358...

work page doi:10.1145/2535838.2535860 2014
[3]

In: Sharygina, N., Veith, H

Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving exist entially quantiﬁed horn clauses. In: Sharygina, N., Veith, H. (eds.) Computer Aided Veriﬁcation. pp. 869–

work page
[4]

Springer Berlin Heidelberg, Berlin, Heidelberg (2013 )

work page 2013
[5]

In: Gallagher, J.P., R¨ ummer, P

Beyene, T.A., Popeea, C., Rybalchenko, A.: Eﬃcient CTL ve riﬁcation via horn constraints solving. In: Gallagher, J.P., R¨ ummer, P. (eds .) Proceedings 3rd Work- shop on Horn Clauses for Veriﬁcation and Synthesis, HCVS@ET APS 2016, Eind- hoven, The Netherlands, 3rd April 2016. EPTCS, vol. 219, pp. 1–14 (2016). https://doi.org/10.4204/EPTCS.219.1, https://...

work page doi:10.4204/eptcs.219.1 2016
[6]

Bj ørner, N., Gurﬁnkel, A., McMillan, K., Rybalchenko, A.: Horn Clause Solvers for Program Veriﬁcation, pp. 24–51. Springer International Pu blishing, Cham (2015)

work page 2015
[8]

Elec- tronic Proceedings in Theoretical Computer Science 260, 4–22 (Nov 2017)

Bloem, R., Schewe, S., Khalimov, A.: CTL* synthesis via LT L synthesis. Elec- tronic Proceedings in Theoretical Computer Science 260, 4–22 (Nov 2017). https://doi.org/10.4204/eptcs.260.4, http://dx.doi.org/10.4204/EPTCS.260.4

work page doi:10.4204/eptcs.260.4 2017
[9]

In: Kroening, D., P˘ as˘ areanu, C.S

Cook, B., Khlaaf, H., Piterman, N.: On automation of CTL* v eriﬁcation for inﬁnite-state systems. In: Kroening, D., P˘ as˘ areanu, C.S. (eds.) Computer Aided Veriﬁcation. pp. 13–29. Springer International Publishin g, Cham (2015)

work page 2015
[10]

In: Ball, T., Jones, R.B

Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Bey ond safety. In: Ball, T., Jones, R.B. (eds.) Computer Aided Veriﬁcation. pp. 415–418 . Springer Berlin Hei- delberg, Berlin, Heidelberg (2006)

work page 2006
[11]

Theoretical Computer Science 126(1), 77–96 (1994)

Dam, M.: CTL ∗ and ECTL ∗ as fragments of the modal µ- calculus. Theoretical Computer Science 126(1), 77–96 (1994). https://doi.org/https://doi.org/10.1016/0304-3975(94)90269-0, https://www.sciencedirect.com/science/article/pii/0304397594902690

work page doi:10.1016/0304-3975(94)90269-0 1994
[12]

72–9 8 (04 2016)

Finkbeiner, B.: Synthesis of reactive systems, pp. 72–9 8 (04 2016). https://doi.org/10.3233/978-1-61499-627-9-72

work page doi:10.3233/978-1-61499-627-9-72 2016
[13]

Founda- tions and Trends® in Programming Languages 4(1-2), 1–119 (2017)

Gulwani, S., Polozov, O., Singh, R.: Program synthesis. Founda- tions and Trends® in Programming Languages 4(1-2), 1–119 (2017). https://doi.org/10.1561/2500000010, http://dx.doi.org/10.1561/2500000010

work page doi:10.1561/2500000010 2017
[14]

Guo, D., Svyatkovskiy, A., Yin, J., Duan, N., Brockschmi dt, M., Allamanis, M.: Learning to complete code with sketches (2022)

work page 2022
[15]

Theoretical Computer Science 331, 397–428 (02 2005)

Kesten, Y., Pnueli, A.: A compositional approach to CTL* ver- iﬁcation. Theoretical Computer Science 331, 397–428 (02 2005). https://doi.org/10.1016/j.tcs.2004.09.023 21

work page doi:10.1016/j.tcs.2004.09.023 2005
[16]

Reducibility Among Combinatorial Problems

Khalimov, A., Bloem, R.: Bounded synthesis for Streett, Rabin, and CTL*. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Veriﬁcat ion - 29th In- ternational Conference, CA V 2017, Heidelberg, Germany, Ju ly 24-28, 2017, Proceedings, Part II. Lecture Notes in Computer Science, vo l. 10427, pp. 333–352. Springer (2017). https://doi.org/10.1007/9 78-3-319...

work page doi:10.1007/9 2017
[17]

Kupferman, O., Vardi, M.Y., Wolper, P.: An automata- theoretic approach to branching-time model checking. J. AC M 47(2), 312–360 (2000). https://doi.org/10.1145/333979.33 3987, https://doi.org/10.1145/333979.333987

work page doi:10.1145/333979.33 2000
[18]

Long, F., Rinard, M.: Staged program repair with conditi on synthesis. pp. 166–178 (08 2015). https://doi.org/10.1145/2786805.2786811

work page doi:10.1145/2786805.2786811 2015
[19]

Theoretical Computer Science 163(1-2), 99–116 (1996)

Niwi´ nski, D., Walukiewicz, I.: Games for the µ-calculus. Theoretical Computer Science 163(1-2), 99–116 (1996)

work page 1996
[20]

In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004

Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004. pp . 32–41 (2004). https://doi.org/10.1109/LICS.2004.1319598

work page doi:10.1109/lics.2004.1319598 2004
[21]

In: Rozier, K.Y., C haudhuri, S

Rothenberg, B.C., Grumberg, O., Vizel, Y., Singher, E.: Condition synthesis real- izability via constrained horn clauses. In: Rozier, K.Y., C haudhuri, S. (eds.) NASA Formal Methods. pp. 380–396. Springer Nature Switzerland, Cham (2023)

work page 2023
[22]

SIGARCH Comput

Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Sar aswat, V.: Com- binatorial sketching for ﬁnite programs. SIGARCH Comput. A rchit. News 34(5), 404–415 (oct 2006). https://doi.org/10.1145/116891 9.1168907, https://doi.org/10.1145/1168919.1168907

work page doi:10.1145/116891 2006
[23]

International Journal on Software Tools for Technology Transfer 15(5), 497–518 (January 2012)

Srivastava, S., Gulwani, S., Foster, J.S.: Template-ba sed program veriﬁcation and program synthesis. International Journal on Software Tools for Technology Transfer 15(5), 497–518 (January 2012)

work page 2012
[24]

Unno, H., Terauchi, T., Gu, Y., Koskinen, E.: Modular pri mal-dual ﬁxpoint logic solving for temporal veriﬁcation. Proc. ACM Program. Lang. 7(POPL) (jan 2023). https://doi.org/10.1145/3571265, https://doi.org/10.1145/3571265

work page doi:10.1145/3571265 2023
[25]

In: Silva, A., Leino, K.R.M

Unno, H., Terauchi, T., Koskinen, E.: Constraint-based relational veriﬁcation. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Veriﬁcation . pp. 742–766. Springer International Publishing, Cham (2021)

work page 2021
[26]

, Zhang, L.: Precise condition synthesis for program repair

Xiong, Y., Wang, J., Yan, R., Zhang, J., Han, S., Huang, G. , Zhang, L.: Precise condition synthesis for program repair. In: 2017 IE EE/ACM 39th In- ternational Conference on Software Engineering (ICSE). pp . 416–426 (2017). https://doi.org/10.1109/ICSE.2017.45

work page doi:10.1109/icse.2017.45 2017
[27]

IEEE Trans

Xuan, J., Martinez, M., DeMarco, F., Clement, M., Marcot e, S.L., Durieux, T., Le Berre, D., Monperrus, M.: Nopol: Automatic r epair of conditional statement bugs in java programs. IEEE Trans. Softw. Eng. 43(1), 34–55 (jan 2017). https://doi.org/10.1109/TSE.2016 .2560811, https://doi.org/10.1109/TSE.2016.2560811 22 A Appendix A.1 Proof of complexity theor...

work page doi:10.1109/tse.2016 2017

[1] [1]

Beyene, T.A., Brockschmidt, M., Rybalchenko, A.: CTL+FO veriﬁcation as con- straint solving (2014)

work page 2014

[2] [2]

In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, ACM, pp

Beyene, T.A., Chaudhuri, S., Popeea, C., Rybalchenko, A. : A constraint-based approach to solving games on inﬁnite graphs. In: Jagannatha n, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Prin ciples of Programming Languages, POPL ’14, San Diego, CA, USA, Janu ary 20- 21, 2014. pp. 221–234. ACM (2014). https://doi.org/10.114 5/25358...

work page doi:10.1145/2535838.2535860 2014

[3] [3]

In: Sharygina, N., Veith, H

Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving exist entially quantiﬁed horn clauses. In: Sharygina, N., Veith, H. (eds.) Computer Aided Veriﬁcation. pp. 869–

work page

[4] [4]

Springer Berlin Heidelberg, Berlin, Heidelberg (2013 )

work page 2013

[5] [5]

In: Gallagher, J.P., R¨ ummer, P

Beyene, T.A., Popeea, C., Rybalchenko, A.: Eﬃcient CTL ve riﬁcation via horn constraints solving. In: Gallagher, J.P., R¨ ummer, P. (eds .) Proceedings 3rd Work- shop on Horn Clauses for Veriﬁcation and Synthesis, HCVS@ET APS 2016, Eind- hoven, The Netherlands, 3rd April 2016. EPTCS, vol. 219, pp. 1–14 (2016). https://doi.org/10.4204/EPTCS.219.1, https://...

work page doi:10.4204/eptcs.219.1 2016

[6] [6]

Bj ørner, N., Gurﬁnkel, A., McMillan, K., Rybalchenko, A.: Horn Clause Solvers for Program Veriﬁcation, pp. 24–51. Springer International Pu blishing, Cham (2015)

work page 2015

[7] [8]

Elec- tronic Proceedings in Theoretical Computer Science 260, 4–22 (Nov 2017)

Bloem, R., Schewe, S., Khalimov, A.: CTL* synthesis via LT L synthesis. Elec- tronic Proceedings in Theoretical Computer Science 260, 4–22 (Nov 2017). https://doi.org/10.4204/eptcs.260.4, http://dx.doi.org/10.4204/EPTCS.260.4

work page doi:10.4204/eptcs.260.4 2017

[8] [9]

In: Kroening, D., P˘ as˘ areanu, C.S

Cook, B., Khlaaf, H., Piterman, N.: On automation of CTL* v eriﬁcation for inﬁnite-state systems. In: Kroening, D., P˘ as˘ areanu, C.S. (eds.) Computer Aided Veriﬁcation. pp. 13–29. Springer International Publishin g, Cham (2015)

work page 2015

[9] [10]

In: Ball, T., Jones, R.B

Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Bey ond safety. In: Ball, T., Jones, R.B. (eds.) Computer Aided Veriﬁcation. pp. 415–418 . Springer Berlin Hei- delberg, Berlin, Heidelberg (2006)

work page 2006

[10] [11]

Theoretical Computer Science 126(1), 77–96 (1994)

Dam, M.: CTL ∗ and ECTL ∗ as fragments of the modal µ- calculus. Theoretical Computer Science 126(1), 77–96 (1994). https://doi.org/https://doi.org/10.1016/0304-3975(94)90269-0, https://www.sciencedirect.com/science/article/pii/0304397594902690

work page doi:10.1016/0304-3975(94)90269-0 1994

[11] [12]

72–9 8 (04 2016)

Finkbeiner, B.: Synthesis of reactive systems, pp. 72–9 8 (04 2016). https://doi.org/10.3233/978-1-61499-627-9-72

work page doi:10.3233/978-1-61499-627-9-72 2016

[12] [13]

Founda- tions and Trends® in Programming Languages 4(1-2), 1–119 (2017)

Gulwani, S., Polozov, O., Singh, R.: Program synthesis. Founda- tions and Trends® in Programming Languages 4(1-2), 1–119 (2017). https://doi.org/10.1561/2500000010, http://dx.doi.org/10.1561/2500000010

work page doi:10.1561/2500000010 2017

[13] [14]

Guo, D., Svyatkovskiy, A., Yin, J., Duan, N., Brockschmi dt, M., Allamanis, M.: Learning to complete code with sketches (2022)

work page 2022

[14] [15]

Theoretical Computer Science 331, 397–428 (02 2005)

Kesten, Y., Pnueli, A.: A compositional approach to CTL* ver- iﬁcation. Theoretical Computer Science 331, 397–428 (02 2005). https://doi.org/10.1016/j.tcs.2004.09.023 21

work page doi:10.1016/j.tcs.2004.09.023 2005

[15] [16]

Reducibility Among Combinatorial Problems

Khalimov, A., Bloem, R.: Bounded synthesis for Streett, Rabin, and CTL*. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Veriﬁcat ion - 29th In- ternational Conference, CA V 2017, Heidelberg, Germany, Ju ly 24-28, 2017, Proceedings, Part II. Lecture Notes in Computer Science, vo l. 10427, pp. 333–352. Springer (2017). https://doi.org/10.1007/9 78-3-319...

work page doi:10.1007/9 2017

[16] [17]

Kupferman, O., Vardi, M.Y., Wolper, P.: An automata- theoretic approach to branching-time model checking. J. AC M 47(2), 312–360 (2000). https://doi.org/10.1145/333979.33 3987, https://doi.org/10.1145/333979.333987

work page doi:10.1145/333979.33 2000

[17] [18]

Long, F., Rinard, M.: Staged program repair with conditi on synthesis. pp. 166–178 (08 2015). https://doi.org/10.1145/2786805.2786811

work page doi:10.1145/2786805.2786811 2015

[18] [19]

Theoretical Computer Science 163(1-2), 99–116 (1996)

Niwi´ nski, D., Walukiewicz, I.: Games for the µ-calculus. Theoretical Computer Science 163(1-2), 99–116 (1996)

work page 1996

[19] [20]

In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004

Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004. pp . 32–41 (2004). https://doi.org/10.1109/LICS.2004.1319598

work page doi:10.1109/lics.2004.1319598 2004

[20] [21]

In: Rozier, K.Y., C haudhuri, S

Rothenberg, B.C., Grumberg, O., Vizel, Y., Singher, E.: Condition synthesis real- izability via constrained horn clauses. In: Rozier, K.Y., C haudhuri, S. (eds.) NASA Formal Methods. pp. 380–396. Springer Nature Switzerland, Cham (2023)

work page 2023

[21] [22]

SIGARCH Comput

Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Sar aswat, V.: Com- binatorial sketching for ﬁnite programs. SIGARCH Comput. A rchit. News 34(5), 404–415 (oct 2006). https://doi.org/10.1145/116891 9.1168907, https://doi.org/10.1145/1168919.1168907

work page doi:10.1145/116891 2006

[22] [23]

International Journal on Software Tools for Technology Transfer 15(5), 497–518 (January 2012)

Srivastava, S., Gulwani, S., Foster, J.S.: Template-ba sed program veriﬁcation and program synthesis. International Journal on Software Tools for Technology Transfer 15(5), 497–518 (January 2012)

work page 2012

[23] [24]

Unno, H., Terauchi, T., Gu, Y., Koskinen, E.: Modular pri mal-dual ﬁxpoint logic solving for temporal veriﬁcation. Proc. ACM Program. Lang. 7(POPL) (jan 2023). https://doi.org/10.1145/3571265, https://doi.org/10.1145/3571265

work page doi:10.1145/3571265 2023

[24] [25]

In: Silva, A., Leino, K.R.M

Unno, H., Terauchi, T., Koskinen, E.: Constraint-based relational veriﬁcation. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Veriﬁcation . pp. 742–766. Springer International Publishing, Cham (2021)

work page 2021

[25] [26]

, Zhang, L.: Precise condition synthesis for program repair

Xiong, Y., Wang, J., Yan, R., Zhang, J., Han, S., Huang, G. , Zhang, L.: Precise condition synthesis for program repair. In: 2017 IE EE/ACM 39th In- ternational Conference on Software Engineering (ICSE). pp . 416–426 (2017). https://doi.org/10.1109/ICSE.2017.45

work page doi:10.1109/icse.2017.45 2017

[26] [27]

IEEE Trans

Xuan, J., Martinez, M., DeMarco, F., Clement, M., Marcot e, S.L., Durieux, T., Le Berre, D., Monperrus, M.: Nopol: Automatic r epair of conditional statement bugs in java programs. IEEE Trans. Softw. Eng. 43(1), 34–55 (jan 2017). https://doi.org/10.1109/TSE.2016 .2560811, https://doi.org/10.1109/TSE.2016.2560811 22 A Appendix A.1 Proof of complexity theor...

work page doi:10.1109/tse.2016 2017