arxiv: 2605.15143 · v1 · submitted 2026-05-14 · 💻 cs.LO · cs.PL

Recognition: 2 theorem links

· Lean Theorem

Complete Local Reasoning About Parameterized Programs Over Topologies

Ruotong Cheng , Azadeh Farzan

Authors on Pith no claims yet

Pith reviewed 2026-05-15 02:54 UTC · model grok-4.3

classification 💻 cs.LO cs.PL

keywords parameterized verificationconcurrent programsinductive invariantscommunication topologiessafety verificationcompositional reasoninglocal proofsdistributed systems

0 comments

The pith

Safety verification of parameterized concurrent programs reduces to complete local proofs under suitable topology assumptions.

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

The paper tackles automatic safety verification for families of concurrent programs that may have infinitely many states and communicate according to arbitrary topologies. It establishes that when the topology meets certain conditions, the global verification task decomposes completely into a finite collection of local proofs that together certify a universally quantified inductive invariant holding for every node. This compositional reduction means one no longer needs to reason directly about the entire parameterized system. The result matters because many distributed systems are naturally expressed as parameterized programs over topologies, yet their correctness proofs have remained difficult to automate without such decompositions. The authors supply an algorithm that computes these local proofs and report that it succeeds on benchmarks spanning multiple topologies.

Core claim

Under reasonable assumptions on the underlying topology, the safety verification problem for parameterized concurrent programs can be reduced to a compositional scheme consisting of a finite set of local proofs that together establish a universally quantified inductive invariant for the entire family. The reduction is complete: success of the local proofs guarantees global safety. An algorithm implementing this scheme is presented and shown effective on benchmarks over several topologies.

What carries the argument

The compositional reduction that decomposes global safety verification of parameterized programs into a finite set of local proofs based on topology structure, yielding a universally quantified inductive invariant.

If this is right

The algorithm automatically constructs the universally quantified inductive invariant needed for the proof.
Verification succeeds for the reported benchmarks across multiple distinct topologies.
The method applies to infinite-state programs because the local proofs avoid explicit global state enumeration.
Once the topology assumptions hold, parameterized safety reduces to checking finitely many local conditions.

Where Pith is reading between the lines

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

The same local-reasoning technique could be tested on liveness properties beyond safety if the topology decomposition extends naturally.
Programs whose topologies evolve over time might admit similar reductions if the changes preserve the key structural properties.
Integration with existing invariant-generation tools could automate the local-proof step for larger case studies.

Load-bearing premise

The communication topology must satisfy structural properties that allow global invariants to be decomposed completely into local proofs.

What would settle it

A specific topology and program pair where the local proofs all succeed yet a concrete global execution trace violates the safety property would show the reduction is incomplete.

Figures

Figures reproduced from arXiv: 2605.15143 by Azadeh Farzan, Ruotong Cheng.

**Figure 2.** Figure 2: Set HT Φ of Hoare triples for Φ Fix vocabularies VNode and VData. For any φ[ν1, . . . , νk] ∈ QF-Ashcroft, topology T, and tuple v ∈ T k , expanding the vocabulary VNode with parameters from T, we can obtain a closed QF-Ashcroft formula φ[v] by substituting v for the free variables. Then, for a given topology T, any Ashcroft assertion Φ := ∀ν. φ[ν] is equivalent to a conjunction V v∈Tk φ[v], and we can r… view at source ↗

**Figure 3.** Figure 3: Constrained Horn Clauses for a single program over topology Ti [PITH_FULL_IMAGE:figures/full_fig_p012_3.png] view at source ↗

**Figure 1.** Figure 1: Resource nodes do not execute code. We add a unary predicate [PITH_FULL_IMAGE:figures/full_fig_p016_1.png] view at source ↗

**Figure 4.** Figure 4: Clauses generated by Algorithm 1 for the star topology. 9 Experimental Results Implementation Our tool, Mosaic, takes as input a number k ∈ N+, a parameterized program over topologies T = {Ti}i∈I over a finite vocabulary V (assuming the indices I are consecutive natural numbers), a parameterized safety specification, and a pair of numbers i, i′ ∈ I with the assumption that all quantifier-free (k + 1)-types… view at source ↗

**Figure 5.** Figure 5: (a) Quantile plot. (b) Scattered plot of optimizations vs baseline. smaller encoding is not necessarily always easier to solve for the backend solver [PITH_FULL_IMAGE:figures/full_fig_p019_5.png] view at source ↗

**Figure 6.** Figure 6: Repeat of Figure1. The atomicity of the code and the fact that ready acts as a token that is passed down the pipeline are significant in the establishment of a manageable invariant. First, observe that one can turn the above statement into an inductive one: ∀vi : vi ▷ right ▷ ready =⇒ vi ▷ right ▷ data = b ▷ data + t − f (4) To prove this, first observe the essential relationship between two neighbours: ∀v… view at source ↗

**Figure 7.** Figure 7: The 15 small programs in the basis of the pipeline example of [PITH_FULL_IMAGE:figures/full_fig_p025_7.png] view at source ↗

read the original abstract

This paper investigates the algorithmic safety verification problem of infinite-state parameterized concurrent programs over a rich set of communication topologies. The goal is to automatically produce a proof of correctness in the form of a universally quantified inductive invariant, where the quantification is over the nodes in the topology. We illustrate that under reasonable assumptions on the underlying topology, the problem can be reduced to and solved as a compositional scheme, that is, the verification of the parameterized family is reduced to a set of local proofs, in a complete manner. We propose a verification algorithm, which is implemented as a tool, and demonstrate through a set of benchmarks over several different topologies that our approach is effective in proving parameterized programs safe.

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 parameterized safety verification to a complete set of local proofs for programs on certain topologies, with a working tool and benchmarks, but the topology assumptions stay too vague to judge how far the completeness actually reaches.

read the letter

The main point is that under some conditions on the network topology, verifying safety for an infinite family of parameterized concurrent programs boils down to checking a finite collection of local properties, and the reduction is claimed to be complete. They implement this as a tool and run it on benchmarks covering several topologies, which is the practical part that stands out from the abstract alone. What they do well is make the compositional approach algorithmic rather than just theoretical, and the benchmarks give some evidence that it scales on the cases they picked without immediate explosion in proof size or time. That is a concrete step beyond prior local-reasoning work that often stopped at manual proofs or narrower topologies. The soft spot is the topology assumptions. The abstract calls them reasonable but does not spell out the exact class of graphs or the closure properties needed for the completeness direction to hold. Without that, it is difficult to tell whether the method covers topologies with long-range dependencies or non-local cycles that would break the local-to-global implication. The lack of reported failed cases or derivation details in the available material also leaves the soundness claim resting on unexamined steps. This work is for people already working on algorithmic verification of parameterized distributed systems who need a push toward automation. A reader focused on tool development or topology-specific invariants would find the reduction and the implementation useful to examine. I would send it to peer review because the core algorithmic idea is grounded enough to merit detailed checking, even though the assumptions section will probably need expansion.

Referee Report

2 major / 1 minor

Summary. The paper claims that safety verification for infinite-state parameterized concurrent programs over communication topologies can be reduced, under reasonable assumptions on the topology, to a complete compositional scheme consisting of a finite set of local proofs; it presents a verification algorithm, implements it as a tool, and reports that the approach succeeds on a set of benchmarks across several topologies.

Significance. If the completeness direction holds under a precisely characterized class of topologies, the result would be significant for parameterized verification: it would provide an automatic route to universally quantified inductive invariants via local reasoning, addressing a core difficulty in verifying infinite families of systems such as distributed protocols.

major comments (2)

[Abstract and opening sections] The central completeness claim (global safety implies existence of local proofs) rests on 'reasonable assumptions on the underlying topology' that are never enumerated as a concrete class of graphs or graph properties (e.g., bounded degree, absence of long cycles, regularity). Without such a characterization it is impossible to determine whether the reduction excludes precisely those topologies that would require additional global invariants.
[Verification algorithm description] No derivation, proof sketch, or reduction steps are supplied showing how the local proofs are generated or why they are sufficient for global safety; the abstract and reported benchmark success therefore leave the soundness of the local-to-global direction unexamined.

minor comments (1)

[Abstract] The abstract would be clearer if it listed the concrete topologies used in the benchmarks and stated the exact number of local proofs required in each case.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments, which help clarify the presentation of our completeness result. We address each major point below and will revise the manuscript accordingly to make the assumptions explicit and include an accessible proof sketch.

read point-by-point responses

Referee: [Abstract and opening sections] The central completeness claim (global safety implies existence of local proofs) rests on 'reasonable assumptions on the underlying topology' that are never enumerated as a concrete class of graphs or graph properties (e.g., bounded degree, absence of long cycles, regularity). Without such a characterization it is impossible to determine whether the reduction excludes precisely those topologies that would require additional global invariants.

Authors: We agree that an explicit characterization is needed. The assumptions in the paper are that the topologies are bounded-degree graphs admitting only finitely many distinct local neighborhood isomorphism types (covering rings, grids, tori, and hypercubes, among others). Under these conditions, global safety reduces to local proofs because any global execution projects to local ones and the finite neighborhood types allow a finite set of local invariants to compose. We will revise the abstract and Section 2 to state this class precisely as 'bounded-degree graphs with finitely many neighborhood types up to isomorphism' and discuss why it excludes topologies requiring non-local invariants. revision: yes
Referee: [Verification algorithm description] No derivation, proof sketch, or reduction steps are supplied showing how the local proofs are generated or why they are sufficient for global safety; the abstract and reported benchmark success therefore leave the soundness of the local-to-global direction unexamined.

Authors: The full manuscript derives the algorithm in Section 3 via a fixed-point computation over local state templates and proves soundness/completeness in Section 5 by showing that local invariants imply global safety via topology-induced composition and that any global invariant projects to local ones. We acknowledge that an early high-level sketch is absent. We will add a concise outline in the introduction: (1) generate candidate local invariants by solving constraints from transitions and neighborhood templates; (2) local-to-global sufficiency follows from the finite neighborhood assumption ensuring every global step is covered by some local proof; (3) completeness by existential abstraction over non-local nodes. revision: yes

Circularity Check

0 steps flagged

No significant circularity; completeness grounded in external topology assumptions

full rationale

The paper claims that under reasonable assumptions on the underlying topology, parameterized verification reduces completely to a finite set of local proofs. No equations, fitted parameters, or self-citations are exhibited in the abstract or described text that would make the claimed reduction equivalent to its inputs by construction. The derivation chain treats topology properties as independent external inputs rather than self-defining or self-citing constructs. This is the normal non-circular case; the completeness result stands or falls on the (unspecified here) topology class but does not reduce tautologically to prior author work or data fits.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on domain assumptions about topologies rather than free parameters or new entities.

axioms (1)

domain assumption reasonable assumptions on the underlying topology enable complete reduction to local proofs
Invoked in the abstract as the premise that makes the compositional scheme complete.

pith-pipeline@v0.9.0 · 5403 in / 1075 out tokens · 46537 ms · 2026-05-15T02:54:42.567055+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

under reasonable assumptions on the underlying topology, the problem can be reduced to and solved as a compositional scheme... verification of the parameterized family is reduced to a set of local proofs, in a complete manner
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

normalized Ashcroft assertion... quantifier-free k-types... representative terms

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

[1]

International Journal on Software Tools for Technology Transfer18(5), 469–473 (Oct 2016)

Abdulla, P.A., Delzanno, G.: Parameterized verification. International Journal on Software Tools for Technology Transfer18(5), 469–473 (Oct 2016). https://doi.or g/10.1007/s10009-016-0424-3

work page doi:10.1007/s10009-016-0424-3 2016
[2]

In: Giacobazzi, R., Berdine, J., Mastroeni, I

Abdulla, P.A., Haziza, F., Holík, L.: All for the Price of Few. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 476–495. Springer, Berlin, Heidelberg (2013). https://doi.org/ 10.1007/978-3-642-35873-9_28

work page doi:10.1007/978-3-642-35873-9_28 2013
[3]

Distributed Computing31(3), 187–222 (Jun 2018)

Aminof,B.,Kotek,T.,Rubin,S.,Spegni,F.,Veith,H.:Parameterizedmodelcheck- ing of rendezvous systems. Distributed Computing31(3), 187–222 (Jun 2018). https://doi.org/10.1007/s00446-017-0302-6

work page doi:10.1007/s00446-017-0302-6 2018
[4]

Information Processing Letters22(6), 307–309 (May 1986)

Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Information Processing Letters22(6), 307–309 (May 1986). https://doi. org/10.1016/0020-0190(86)90071-2

work page doi:10.1016/0020-0190(86)90071-2 1986
[5]

(eds.) Computer Aided Verification

Arons, T., Pnueli, A., Ruah, S., Xu, Y., Zuck, L.: Parameterized Verification with Automatically Computed Inductive Assertions? In: Berry, G., Comon, H., Finkel, A. (eds.) Computer Aided Verification. pp. 221–234. Springer, Berlin, Heidelberg (2001). https://doi.org/10.1007/3-540-44585-4_19

work page doi:10.1007/3-540-44585-4_19 2001
[6]

In: Badger, J.M., Rozier, K.Y

Ashmore, R., Gurfinkel, A., Trefler, R.: Local Reasoning for Parameterized First Order Protocols. In: Badger, J.M., Rozier, K.Y. (eds.) NASA Formal Methods. pp. 36–53. Springer International Publishing, Cham (2019). https://doi.org/10.1007/ 978-3-030-20652-9_3

work page 2019
[7]

In: Enea, C., Lal, A

Blicha, M., Britikov, K., Sharygina, N.: The Golem Horn Solver. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. pp. 209–223. Springer Nature Switzerland, Cham (2023). https://doi.org/10.1007/978-3-031-37703-7_10 22 Ruotong Cheng and Azadeh Farzan

work page doi:10.1007/978-3-031-37703-7_10 2023
[8]

Communica- tions of the ACM22(5), 281–283 (May 1979)

Chang, E., View Profile, Roberts, R., View Profile: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Communica- tions of the ACM22(5), 281–283 (May 1979). https://doi.org/10.1145/359104.3 59108

work page doi:10.1145/359104.3 1979
[9]

https://doi.org/10.48550/arXiv.2601.18745

Cheng, R., Farzan, A.: Symmetric Proofs of Parameterized Programs (Jan 2026). https://doi.org/10.48550/arXiv.2601.18745

work page doi:10.48550/arxiv.2601.18745 2026
[10]

In: Ramakrishnan, C.R., Rehof, J

de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Sys- tems. pp. 337–340. Springer, Berlin, Heidelberg (2008). https://doi.org/10.1007/ 978-3-540-78800-3_24

work page 2008
[11]

In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 85–94. POPL ’95, Association for Computing Machinery, New York, NY, USA (Jan 1995). https://doi.org/10.1145/199448.199468

work page doi:10.1145/199448.199468 1995
[12]

In: Proceedings of the 31st ACM SIGPLAN Conference on Pro- gramming Language Design and Implementation

Emmi, M., Majumdar, R., Manevich, R.: Parameterized verification of transac- tional memories. In: Proceedings of the 31st ACM SIGPLAN Conference on Pro- gramming Language Design and Implementation. pp. 134–145. PLDI ’10, As- sociation for Computing Machinery, New York, NY, USA (Jun 2010). https: //doi.org/10.1145/1806596.1806613

work page doi:10.1145/1806596.1806613 2010
[13]

In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Prin- ciples of Programming Languages

Farzan, A., Kincaid, Z., Podelski, A.: Proof Spaces for Unbounded Parallelism. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Prin- ciples of Programming Languages. pp. 407–420. ACM, Mumbai India (Jan 2015). https://doi.org/10.1145/2676726.2677012

work page doi:10.1145/2676726.2677012 2015
[14]

Proceedings of the ACM on Programming Languages8(POPL), 2485–2513 (Jan 2024)

Farzan, A., Klumpp, D., Podelski, A.: Commutativity Simplifies Proofs of Parame- terized Programs. Proceedings of the ACM on Programming Languages8(POPL), 2485–2513 (Jan 2024). https://doi.org/10.1145/3632925

work page doi:10.1145/3632925 2024
[15]

In: Legay, A., Margaria, T

Feldman, Y.M.Y., Padon, O., Immerman, N., Sagiv, M., Shoham, S.: Bounded Quantifier Instantiation for Checking Inductive Invariants. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 76–95. Springer, Berlin, Heidelberg (2017). https://doi.org/10.1007/978-3-662-5 4577-5_5

work page doi:10.1007/978-3-662-5 2017
[16]

In: Proceedings of the 33rd ACM SIGPLAN Confer- ence on Programming Language Design and Implementation

Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing soft- ware verifiers from proof rules. In: Proceedings of the 33rd ACM SIGPLAN Confer- ence on Programming Language Design and Implementation. pp. 405–416. PLDI ’12, Association for Computing Machinery, New York, NY, USA (Jun 2012). https://doi.org/10.1145/2254064.2254112

work page doi:10.1145/2254064.2254112 2012
[17]

In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering

Gurfinkel, A., Shoham, S., Meshman, Y.: SMT-based verification of parameter- ized systems. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. pp. 338–348. FSE 2016, Association for Computing Machinery, New York, NY, USA (Nov 2016). https: //doi.org/10.1145/2950290.2950330

work page doi:10.1145/2950290.2950330 2016
[18]

Haziza, F.: Few is Just Enough! : Small Model Theorem for Parameterized Verifi- cation and Shape Analysis (2015)

work page 2015
[19]

Cambridge University Press, Cambridge ; New York (1997)

Hodges, W.: A Shorter Model Theory. Cambridge University Press, Cambridge ; New York (1997)

work page 1997
[20]

In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

Hoenicke, J., Majumdar, R., Podelski, A.: Thread modularity at many levels: A pearl in compositional verification. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. pp. 473–485. ACM, Paris France (Jan 2017). https://doi.org/10.1145/3009837.3009893 Complete Local Reasoning About Parameterized Programs Over Topologies 23

work page doi:10.1145/3009837.3009893 2017
[21]

In: 2018 Formal Methods in Computer Aided Design (FMCAD)

Hojjat, H., Rümmer, P.: The ELDARICA Horn Solver. In: 2018 Formal Methods in Computer Aided Design (FMCAD). pp. 1–7 (Oct 2018). https://doi.org/10.239 19/FMCAD.2018.8603013

work page arXiv 2018
[22]

EPTCS169, 39–52 (2014)

Hojjat, H., Rümmer, P., Subotic, P., Yi, W.: Horn Clauses for Communicating Timed Systems. EPTCS169, 39–52 (2014)

work page 2014
[23]

In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Imple- mentation, pp

Koenig, J.R., View Profile, Padon, O., View Profile, Immerman, N., View Profile, Aiken, A., View Profile: First-order quantified separators. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Imple- mentation, pp. 703–717. ACM Conferences (Jun 2020). https://doi.org/10.1145/ 3385412.3386018

work page arXiv 2020
[24]

Formal Methods in System Design48(3), 175–205 (Jun 2016)

Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods in System Design48(3), 175–205 (Jun 2016). https: //doi.org/10.1007/s10703-016-0249-4

work page doi:10.1007/s10703-016-0249-4 2016
[25]

Texts in Theoretical Computer Science

Kroening, D., Strichman, O.: Decision Procedures. Texts in Theoretical Computer Science. An EATCS Series, Springer Berlin Heidelberg, Berlin, Heidelberg (2016). https://doi.org/10.1007/978-3-662-50497-0

work page doi:10.1007/978-3-662-50497-0 2016
[26]

Springer Berlin Heidelberg, Berlin, Heidelberg (2004)

Libkin, L.: Elements of Finite Model Theory. Springer Berlin Heidelberg, Berlin, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07003-1

work page doi:10.1007/978-3-662-07003-1 2004
[27]

In: Rival, X

Monniaux, D., Gonnord, L.: Cell Morphing: From Array Programs to Array-Free Horn Clauses. In: Rival, X. (ed.) Static Analysis. pp. 361–382. Springer, Berlin, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53413-7_18

work page doi:10.1007/978-3-662-53413-7_18 2016
[28]

In: Cook, B., Podelski, A

Namjoshi, K.S.: Symmetry and Completeness in the Analysis of Parameterized Systems. In: Cook, B., Podelski, A. (eds.) Verification, Model Checking, and Ab- stract Interpretation. pp. 299–313. Springer, Berlin, Heidelberg (2007). https: //doi.org/10.1007/978-3-540-69738-1_22

work page doi:10.1007/978-3-540-69738-1_22 2007
[29]

In: Kuncak, V., Rybalchenko, A

Namjoshi, K.S., Trefler, R.J.: Local Symmetry and Compositional Verification. In: Kuncak, V., Rybalchenko, A. (eds.) Verification, Model Checking, and Abstract In- terpretation, vol. 7148, pp. 348–362. Springer Berlin Heidelberg, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27940-9_23

work page doi:10.1007/978-3-642-27940-9_23 2012
[30]

In: Chechik, M., Raskin, J.F

Namjoshi, K.S., Trefler, R.J.: Parameterized Compositional Model Checking. In: Chechik, M., Raskin, J.F. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 589–606. Springer, Berlin, Heidelberg (2016). https://do i.org/10.1007/978-3-662-49674-9_39

work page doi:10.1007/978-3-662-49674-9_39 2016
[31]

In: Beyer, D., Huisman, M

Namjoshi, K.S., Trefler, R.J.: Symmetry Reduction for the Local Mu-Calculus. In: Beyer, D., Huisman, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 379–395. Springer International Publishing, Cham (2018). https://doi.org/10.1007/978-3-319-89963-3_22

work page doi:10.1007/978-3-319-89963-3_22 2018
[32]

ACM SIGPLAN Notices51(6), 614–630 (Jun 2016)

Padon, O., View Profile, McMillan, K.L., View Profile, Panda, A., View Pro- file, Sagiv, M., View Profile, Shoham, S., View Profile: Ivy: Safety verification by interactive generalization. ACM SIGPLAN Notices51(6), 614–630 (Jun 2016). https://doi.org/10.1145/2980983.2908118

work page doi:10.1145/2980983.2908118 2016
[33]

yuTf8gLzKrmv3kYA1F0NEEKZWKE=

Pnueli, A., Ruah, S., Zuck, L.: Automatic Deductive Verification with Invisible Invariants. In: Margaria, T., Yi, W. (eds.) Tools and Algorithms for the Con- struction and Analysis of Systems. pp. 82–97. Springer, Berlin, Heidelberg (2001). https://doi.org/10.1007/3-540-45319-9_7 24 Ruotong Cheng and Azadeh Farzan A The Pipeline Example First note that to...

work page doi:10.1007/3-540-45319-9_7 2001
[34]

, νk]and tuplev∈T ′k, ifµ|= φ(v), thenβ ∗µ|=φ(β −1(v))

For anyQF-Ashcroftformulaφ[ν 1, . . . , νk]and tuplev∈T ′k, ifµ|= φ(v), thenβ ∗µ|=φ(β −1(v))

work page
[35]

Proof.Letφ[ν 1,

For any Ashcroft assertionΦ, ifµ|=Φ, thenβ ∗µ|=Φ. Proof.Letφ[ν 1, . . . , νk]be aQF-Ashcroftformula and tuplev∈T ′k. State- ment 1 can be shown by induction on the structure ofφ. For instance, as a base case, ifφis a formula of the formϕ[µ(ν1), . . . ,µ(νk)], whereϕis aV Data-formula, then µ|=φ(v)⇐ ⇒D|=ϕ(µ(v 1), . . . , µ(vk)) ⇐ ⇒D|=ϕ((β ∗µ)(β−1(v1)), . ....

work page
[36]

, Tm inT, and everyT r is definable by a quantifier-free formulaαr, i.e., for anyV-structureTand v∈T k, we haveT|=α r(v)⇐ ⇒qftype(T,v) =T r

There are finitely many quantifier-freek-typesT1, . . . , Tm inT, and everyT r is definable by a quantifier-free formulaαr, i.e., for anyV-structureTand v∈T k, we haveT|=α r(v)⇐ ⇒qftype(T,v) =T r. Moreover, the formula defining the quantifier-freek-type of a given node tuple inTis computable

work page
[37]

Any quantifier-free formula withkfree variables is equivalent overTto a disjunction of a subset of theαr’s. Proof.1. LetT∈ Tandv∈T k. For eachu∈N(v), lett u[ν]be aV-term of minimal height such thatt u(v) =u. Letαbe the conjunction of the following formulas: –tvi =ν i for eachi∈ {1, . . . , k}; –tu1 ̸=t u2 for all distinctu1, u2 ∈N(v); –for all relation sy...

work page
[38]

Letϕbe a quantifier-free formula withkvariables

Combining 1 and Proposition 1, we have that any≃-equivalence class of node tuples of lengthkinTis definable by someα r. Letϕbe a quantifier-free formula withkvariables. The class of node tu- ples inTdefined byϕis closed under≃-equivalence. Thus, it is a union of≃-equivalence classes. Take the disjunction of theα r’s that define each equivalence class.⊓ ⊔ ...

work page