Pith. sign in

REVIEW 4 major objections 4 minor 43 references

VeraRAN: Pre-Actuation Certification and Event-Causal Synchronization Repair for Asynchronous Multi-Interface RAN Plans

T0 review · 4 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper argues that asynchronous RAN plans are certifiable only by exploring full lifecycle event interleavings, and that only the authoritative APPLY event may discharge cross-path dependencies.

desk verdict VeraRAN's event-causal certification idea is genuinely new and the paper is honestly scoped; the main risks are unvalidated delay envelopes and missing artifact, not the core logic. read the letter →

arxiv 2608.01047 v3 pith:PE3L6NVD submitted 2026-08-02 cs.NI

Yinghan Hou , Zongyou Yang This is my paper · ORCID
classification cs.NI
keywords O-RANasynchronousactuationeventcontractspre-actuationcertificationsynchronizationrepairpartial-orderreductionagenticRANcontrolmodelchecking
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper argues that a radio access network plan is safe to actuate only if every interleaving of its lifecycle events—request, delivery, acceptance, application, completion, and observation—is checked under bounded delay envelopes, and that only the authoritative APPLY event, or a contract-backed event downstream of it, may release a dependent action. In a frozen study of a 35B planner, 28.8% of 177 locally valid plans admitted an unsafe asynchronous execution even though every command and the target state were valid. The paper introduces VeraRAN, which certifies plans before actuation by exploring admissible event orders, and VeraSync, which inserts versioned event barriers to repair counterexamples and then re-certifies the whole plan. If the claim is right, local validity does not compose into safe asynchronous trajectories, and fixed waits or transport acknowledgements are not safe release authority.

What carries the argument

The per-action event contract $\Gamma_a = (V_a, F_a, \delta_a, \kappa_a, T_a)$ is the central object: a causal DAG over the six lifecycle events REQUEST, DELIVERY, ACCEPT, APPLY, COMPLETE, and OBSERVE, with edge delay bounds $\delta_a$ and evidence signatures $\kappa_a$. The verifier explores all admissible endpoints, delays, versions, and equal-time orders within these contracts. VeraSync's symbolic barrier $B(b,a; z, G)$ opens gate $G$ of action $a$ only after $z \in \mathrm{Auth}(\Gamma_b)$ fires, where $\mathrm{Auth}(\Gamma_b)$ is the authoritative event set consisting of the APPLY event plus any contract-downstream event with matching signature; MI-POR prunes independent interleavings using lifecycle, evidence, resource, repair, and rollback footprints while preserving the verdict.

What would settle it

Instrument a live E2 endpoint that honors its registered contract and observe ACCEPT-to-APPLY separation exceeding the registered upper bound $U_s(\text{APPLY})$ for a dependent action; if a gate released by an OBSERVE event downstream of APPLY fires before the late APPLY and an unsafe intermediate state results, the delay-envelope premise fails. Alternatively, delete one resource conflict from the access map $M$ and show that MI-POR prunes an interleaving that the exact six-event reference flags unsafe.

Watch

Extended reading notes

Core claim

Certification is defined as: all executions in $\mathrm{Exec}(P)$ satisfy the safety property $\Phi_S$ and at least one execution satisfies the bounded completion property $\Phi_L$ (Eqs. 2 and 3). VeraSync's barriers make a repaired plan pass this check by ordering the successor's REQUEST or APPLY gate behind the predecessor's authoritative event, and the runtime executor opens a gate only when evidence matches the required action, scope, version, and epoch. The live E2 audit shows ACCEPT may precede APPLY, so ACCEPT alone is not authoritative; completion signals released a dependency only when the registered event contract places them causally downstream of APPLY.

Load-bearing premise

The certificate is only as strong as the registered delay envelopes and the resource access map: if a real endpoint applies an event later than its registered upper bound, or the access map omits a dependency, a certified plan can still be unsafe live.

Editorial extensions

If this is right

  • Controllers can actuate certified plans asynchronously without global serialization: after VeraSync repair, 86.98% of action pairs remain unordered with portable REQUEST gates and 89.33% with registered application hooks.
  • Fixed-wait release is unsafe under envelope shift: in the delay-shift sweep a 120 ms wait protected 30/30 nominal but only 23/30 stressed runs, while direct APPLY protected 30/30 in both.
  • ACCEPT-only release is not generally authoritative: it protected 0/30 quota-migration runs and 30/30 handover runs only through an incidental fixed path delay.
  • Bounded completion is a separate certification obligation: a gate that never sees matching authoritative evidence stays closed until manifest expiry rather than releasing unsafely.
  • MI-POR reduces certification cost by 94.6–95.0% explored states on 20–40-action plans while matching exact verdicts, first violations, and completion extrema.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The event-causal release principle likely generalizes beyond RAN to other distributed control planes: any synthesized synchronization order should be bound to the authoritative state transition of the predecessor, not to a transport acknowledgement.
  • If delay envelopes are maintained as registered artifacts, the same certificate pipeline could be reused across planners, making plan safety independent of which language model or optimizer produced the plan.
  • The delay-shift results suggest a practical operational extension: monitor envelope drift per endpoint and re-certify when measured APPLY times approach the registered upper bound, rather than assuming static contracts.
  • A sharp audit of the access map would strengthen the MI-POR claim: deleting one resource conflict from the registry and checking whether the reduced verifier flips a known unsafe plan to safe.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. VeraRAN is a pre-actuation certification framework for asynchronous multi-interface RAN control plans. Each action is compiled into a typed event contract covering REQUEST, DELIVERY, ACCEPT, APPLY, COMPLETE, and OBSERVE, with registered delay envelopes and endpoint choices. The verifier explores all bounded executions in Exec(P) and certifies a plan only if every execution satisfies the safety property and every execution reaches completion (Eqs. 2–3). When a counterexample is found, VeraSync inserts versioned event gates and re-runs the whole-plan verification. MI-POR is a partial-order reduction that prunes independent interleavings using lifecycle, resource, evidence, repair, and rollback footprints. The evaluation includes a frozen planner study (51/177 locally valid 35B plans are asynchronously unsafe), a 144-plan post-freeze confirmation within the authors' repair domain, ns-O-RAN replay, a 30-control live E2 audit, and MI-POR state-reduction measurements on 20–100-action workloads.

Significance. If the result holds, the paper makes a useful contribution to O-RAN control verification by identifying and formalizing a real gap: locally valid commands do not compose into safe asynchronous trajectories, and release authority should be tied to the authoritative APPLY event or a contract-backed event causally downstream of APPLY. Theorem 1 and Lemma 1 are simple and clean, and the central claim does not reduce to a fitted parameter. The evaluation is carefully scoped with a frozen protocol, pre-registered hash, baseline comparisons, and independent live measurements, which gives the empirical claims more weight than a purely simulated study. The main caveats are that the MI-POR correctness proof is presented as a series of proof sketches, and that the deployment guarantee is explicitly conditional on registered delay envelopes and access-map soundness. The 144/144 confirmation is a self-evaluation within the authors' own declared repair domain, so it should not be read as evidence of generalization to independently specified RAN plan families.

major comments (4)
  1. [Section V-B (Theorem 2, Lemmas 2–6)] The correctness of MI-POR is load-bearing for the scalability contribution, but Theorem 2 is supported only by proof sketches. Lemma 4 asserts that the implemented conflict detector establishes independence under AccessSound, and Lemma 6 asserts that every execution can be transformed by adjacent independence swaps; neither proof addresses how the canonical key Xi interacts with the schedule-extension behavior of newly enabled successors, nor how the future closure handles all possible same-tick enablements. Please provide complete proofs, or a machine-checked formalization, and state precisely which parts of the proof are verified by the exact-versus-reduced differential tests in Section VII-E.
  2. [Section IV-B (Algorithm 1)] The completeness statement for the repair loop is given for an uncapped loop ('terminates within |B_T(P)| iterations or returns UNSUPPORTED'), but Algorithm 1 fixes Kmax = 4 and returns ITERATION-LIMIT at k = Kmax. A plan needing five repair iterations would therefore not be certified, so the stated termination/completeness guarantee does not hold for the shipped algorithm. Please either remove the cap from the algorithm, state the cap as a practical performance limit, or prove that Kmax = 4 cannot be reached for the declared template library that is used in the evaluation.
  3. [Section VII-A and VII-F] The safety certificate is conditional on the registered delay envelopes being true upper bounds and on the access map M being sound. The evaluation uses 'symbolic stress bounds' for DELIVERY/APPLY/OBSERVE intervals, and Section VII-D measures only 30 OCUDU controls; it does not measure the tail of the E2/A1/O1 delay distributions or independently verify that every resource dependency of a real deployment is present in M. As stated in Section VII-F, a certified plan can be unsafe in the field if an endpoint fires after U_s(z) or if a dependency is missing from the access map. The paper should either strengthen the empirical grounding by measuring tail behavior and access-map completeness, or state more prominently that the deployment guarantee is conditional on these registry assumptions rather than being a standalone safety certificate.
  4. [Section VII-C] The 144/144 re-certification is a self-evaluation within the authors' own declarative repair domain: the confirmation plans are generated from the same template families that define the repair language, and the oracle evaluates only the declared APPLY-to-APPLY sublanguage. This makes the result a consistency check of the template-guided repair loop rather than evidence of generalization to independently specified RAN control plans. Please add a clear statement of this scope limitation, or provide a held-out/external plan set to support a broader generalization claim.
minor comments (4)
  1. [Section III-A, Eq. (1)] The version identifiers v_h and v_s appear in Eq. (1) without being defined at first use; please define them (e.g., as per-action version tokens) when the typed plan is introduced.
  2. [Section VII-A and Fig. 2(b)] The text says 'Figure 2(b) reports the aligned policy' but the caption is not explicit about which curves correspond to the declared TTL versus the aligned TTL policy; please clarify the labeling.
  3. [Section VII-C] The sentence 'none of its 1,400 barriers can be deleted' is strong; please state explicitly whether deletion was attempted for every barrier individually and what criterion ('certification would fail') was used.
  4. [Section VI(a)] The trusted-computing-base list is informative but would benefit from a small diagram or table showing which components sign or validate which parts of the certificate manifest chi, especially since Section IV-B describes the manifest as registry-bound rather than a proof trace.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the certification claim is explicitly conditional on registered delay envelopes and access maps, and the key event-ordering claims are grounded by live E2 measurement and exact-versus-reduced differential tests rather than by self-citation or fitted parameters.

full rationale

VeraRAN's formal claim is conditional: for a compiled plan P with registered contracts Gamma, delay bounds D, access map M, and declared properties Phi, certification means every execution in Exec(P) satisfies Phi_S and at least one satisfies Phi_L (Eqs. 2-3). The transition system fixes scheduled firing times within [L_s(z), U_s(z)] and forbids TICK when due events exist, so the guarantee is explicitly relative to the registered envelopes and access-map soundness. The live OCUDU E2 audit and ns-O-RAN replay provide independent evidence for the event-ordering model (ACCEPT before APPLY, COMPLETE downstream of APPLY), and the MI-POR theorems (Lemmas 4-6, Theorem 2) are proved relative to AccessSound/EnableSound with exact-versus-reduced differential tests and mutation audits. The 144/144 repair confirmation is a self-evaluation on author-generated plans within the declared repair domain, but it is reported as a repair-capability result, not as an external prediction, and no fitted parameter is renamed as a prediction. I found no load-bearing self-citation chain: the reference list contains no prior work by Hou and Yang, and the design choices (event contracts, APPLY authority, barriers) are argued from mechanism evidence rather than from an author-imposed uniqueness theorem. The principal limitations (delay envelopes as symbolic stress bounds; AccessSound completeness) are explicitly acknowledged in Sections VII-A and VII-F and are assumption-boundary issues, not circular derivations.

Assumptions & free parameters 2 free parameters · 4 assumptions · 0 invented entities

The paper introduces no new physical entities. Its load-bearing assumptions are the event-contract abstraction, the delay envelopes, and the access-map registry conditions that make the partial-order reduction sound.

free parameters (2)
  • Horizon H and evidence TTL = H=64, TTL=64; sensitivity H=64/96/128
    Chosen by the authors as the default evaluation configuration, not fitted to data. Certification and completion results are relative to these bounds.
  • Delay envelopes for E2/A1/O1 = DELIVERY 0-1/1-2/1-3 ticks; APPLY 1-2, handover prepare 1-3; OBSERVE 0-1/1-2
    Symbolic stress bounds chosen by the authors. Safety and completion claims hold only if real endpoint delays lie inside these envelopes.
assumptions (4)
  • domain assumption Per-action event contracts with six event types and APPLY as the only authoritative state-changing event
    Adopted in Section III-A. The entire certificate and repair mechanism depends on this lifecycle model being a faithful abstraction of E2/A1/O1 behavior.
  • domain assumption Registered delay bounds D and delta_a are honored by endpoints within the horizon
    Invoked in Section VII-F. If endpoints exceed the envelope, bounded completion and the safety certificate may not hold live.
  • domain assumption AccessSound(M) and EnableSound(P,B,M) registry conditions hold for MI-POR
    Definitions 2 and the EnableCover condition in Section V. Theorem 2 is registry-relative, so a missing access or same-tick enabling dependency would make the reduction unsound.
  • domain assumption No quota mutations beyond the declared migration during Lemma 1's scope
    Lemma 1 assumes no other mutation of these quotas during the migration and reliable execution of issued actions. The proof is a simple sum argument under these constraints.

how reviews work

0 comments
Cite this review

Pith. "Pith review of VeraRAN: Pre-Actuation Certification and Event-Causal Synchronization Repair for Asynchronous Multi-Interface RAN Plans." pith.science (2026). https://pith.science/paper/PE3L6NVD

@misc{pith2026260801047,
  author       = {Pith},
  title        = {Pith review of: VeraRAN: Pre-Actuation Certification and Event-Causal Synchronization Repair for Asynchronous Multi-Interface RAN Plans},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PE3L6NVD}},
  note         = {Machine review of arXiv:2608.01047}
}
read the original abstract

Agentic RAN controllers combine mobility, energy, and resource actions across independently implemented interfaces. Even when each command is valid and the target state is safe, asynchronous actuation can drive the network through unsafe intermediate states. In a frozen study of a 35B planner, 28.8% of locally valid plans remained asynchronously unsafe. We introduce VeraRAN, which checks plans before actuation by modeling request, delivery, acceptance, application, completion, and observation for each action while exploring plausible delays and event orders. When VeraRAN finds a counterexample, VeraSync inserts versioned event barriers and rechecks the repaired plan for safety and completion. MI-POR prunes independent interleavings using RAN lifecycle and resource footprints. In a post-freeze stratified confirmation within the declared repair domain, VeraSync re-certified every confirmation plan while leaving 87% of action pairs unordered. MI-POR matched exact search in a property-stratified audit and reduced explored states by 94.6-95.0% on 20-40-action plans. Native ns-O-RAN replay and an independent live E2 audit showed why distinguishing these events matters: acceptance may precede the authoritative state transition, so dependent actions must wait for direct APPLY evidence or a contract-backed completion event causally downstream of APPLY.

Figures

Figures reproduced from arXiv: 2608.01047 by the authors.

Figure 1
Figure 1. VeraRAN architecture and event-causal execution. The verifier certifies a candidate plan or sends its counterexample to VeraSync for repair with registered templates and full re-certification. The executor releases a gated REQUEST or opens a registered application hook only on authoritative evidence matching the certified action, scope, version, and epoch. B. Release authority Only APPLY changes authoritative state.… view at source ↗
Figure 2
Figure 2. Local validity leaves trajectory risk that sparse repair can close. (a) Matched planner outputs with Wilson 95% intervals. (b) Application-gate repair and release baselines on 144 confirmations; boxes show median/IQR, whiskers P5–P95, and crosses plans beyond 2H. state, and labels; TICK occurs only for an empty due set. Under LocalityOK, C⊕ returns U iff a component does; absent U, it returns I iff a component does … view at source ↗
Figure 3
Figure 3. Authoritative release adapts to actuation delay. (a) Fixed-wait/direct-APPLY sweep (480 runs). (b) Mechanism-grounded release replay; each mark is one matched run (300 runs). (c) Live E2 ACCEPT-to-APPLY separation (30 controls). Both planners share state, goal, prompt, schema, compiler, verifier, properties, and request seed; all calls compile. A plan is local-pass when its schema, identifiers, action en￾velope, ini… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: MI-POR reduces certification cost at both stages. (a) Median wall time, P5–P95, and states (20 runs per size). (b) Residual Stage 2 savings; cells include absolute median seconds and P5–P95, with a decomposable control below. APPLY remains 30/30 and finishes 62 ms soon…

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

43 extracted references · 1 linked inside Pith

  1. [1]

    Toward dynamic energy- efficient operation of cellular network infrastructure,

    E. Oh, B. Krishnamachari, X. Liu, and Z. Niu, “Toward dynamic energy- efficient operation of cellular network infrastructure,”IEEE Communi- cations Magazine, vol. 49, no. 6, pp. 56–61, 2011

    2011

  2. [2]

    Energy-efficient wireless communications: Tutorial, survey, and open issues,

    G. Y . Li, Z. Xu, C. Xiong, C. Yang, S. Zhanget al., “Energy-efficient wireless communications: Tutorial, survey, and open issues,”IEEE Wireless Communications, vol. 18, no. 6, pp. 28–35, 2011

    2011

  3. [3]

    Multi- tenant radio access network slicing: Statistical multiplexing of spatial loads,

    P. Caballero, A. Banchs, G. de Veciana, and X. Costa-P ´erez, “Multi- tenant radio access network slicing: Statistical multiplexing of spatial loads,”IEEE/ACM Transactions on Networking, vol. 25, no. 5, pp. 3044– 3058, 2017

    2017

  4. [4]

    O-RAN: Disrupting the vir- tualized RAN ecosystem,

    A. Garcia-Saavedra and X. Costa-P ´erez, “O-RAN: Disrupting the vir- tualized RAN ecosystem,”IEEE Communications Standards Magazine, vol. 5, no. 4, pp. 96–103, 2021

    2021

  5. [5]

    Under- standing O-RAN: Architecture, interfaces, algorithms, security, and re- search challenges,

    M. Polese, L. Bonati, S. D’Oro, S. Basagni, and T. Melodia, “Under- standing O-RAN: Architecture, interfaces, algorithms, security, and re- search challenges,”IEEE Communications Surveys & Tutorials, vol. 25, no. 2, pp. 1376–1411, 2023

    2023

  6. [6]

    Open RAN xApps design and evaluation: Lessons learnt and identi- fied challenges,

    M. Hoffmann, S. Janji, A. Samorzewski, L. Kulacz, C. Adamczyket al., “Open RAN xApps design and evaluation: Lessons learnt and identi- fied challenges,”IEEE Journal on Selected Areas in Communications, vol. 42, no. 2, pp. 473–486, 2024

    2024

  7. [7]

    E2 interface: Application protocol (E2AP),

    O-RAN Alliance, “E2 interface: Application protocol (E2AP),” O-RAN Alliance, Tech. Rep. O-RAN.WG3.E2AP-R003-v03.00, 2023

    2023

  8. [8]

    A1 interface: General aspects and principles,

    ETSI, “A1 interface: General aspects and principles,” European Telecommunications Standards Institute, Tech. Rep. ETSI TS 103 983 V3.1.0, Jan. 2024, o-RAN.WG2.A1GAP-R003-v03.01

    2024

Show all 43 references
  1. [9]

    O-RAN operations and maintenance interface specification,

    ——, “O-RAN operations and maintenance interface specification,” European Telecommunications Standards Institute, Tech. Rep. ETSI TS 104 043 V11.0.0, Jun. 2024, o-RAN.WG10.O1-Interface-R003-v11.00

    2024

  2. [10]

    Intelli- gence and learning in O-RAN for data-driven NextG cellular networks,

    L. Bonati, S. D’Oro, M. Polese, S. Basagni, and T. Melodia, “Intelli- gence and learning in O-RAN for data-driven NextG cellular networks,” IEEE Communications Magazine, vol. 59, no. 10, pp. 21–27, 2021

    2021

  3. [11]

    AgentRAN: An agentic AI architecture for autonomous control of open 6G networks,

    M. Elkael, S. D’Oro, L. Bonati, M. Polese, Y . Leeet al., “AgentRAN: An agentic AI architecture for autonomous control of open 6G networks,” IEEE Communications Magazine, pp. 1–7, 2026, early access

    2026

  4. [12]

    ns-O- RAN: Simulating O-RAN 5G systems in ns-3,

    A. Lacava, M. Bordin, M. Polese, R. Sivaraj, T. Zugnoet al., “ns-O- RAN: Simulating O-RAN 5G systems in ns-3,” inProc. Workshop on ns-3, 2023, pp. 35–44

    2023

  5. [13]

    5G; NR; radio resource control (RRC); protocol specification,

    ETSI, “5G; NR; radio resource control (RRC); protocol specification,” European Telecommunications Standards Institute, Tech. Rep. ETSI TS 138 331 V18.6.0, Jul. 2025, 3GPP TS 38.331 Release 18

    2025

  6. [14]

    E2 service model (E2SM) RAN control,

    O-RAN Alliance, “E2 service model (E2SM) RAN control,” O-RAN Alliance, Tech. Rep. O-RAN.WG3.E2SM-RC-R003-v03.00, 2023

    2023

  7. [15]

    OCUDU: Open-source 5G and beyond CU/DU,

    OCUDU Project, “OCUDU: Open-source 5G and beyond CU/DU,” https://gitlab.com/ocudu/ocudu, 2026, revision 9b0cfa600d9d693bf56277e4575dc8c4b8b729bb; accessed July 2026

    2026

  8. [16]

    Qwen3.6-35B-A3B model card,

    Qwen Team, “Qwen3.6-35B-A3B model card,” https://huggingface. co/Qwen/Qwen3.6-35B-A3B, 2026, experimental revision 1a5ae24e867f8d82388070d3f61590158a01d15c; accessed July 2026

    2026

  9. [17]

    Qwen3-4B-Instruct-2507 model card,

    ——, “Qwen3-4B-Instruct-2507 model card,” https:// huggingface.co/Qwen/Qwen3-4B-Instruct-2507, 2025, revision cdbee75f17c01a7cc42f958dc650907174af0554; accessed July 2026

    2025

  10. [18]

    PACIFISTA: Conflict evaluation and management in open RAN,

    P. B. del Prever, S. D’Oro, L. Bonati, M. Polese, M. Tsampaziet al., “PACIFISTA: Conflict evaluation and management in open RAN,”IEEE Transactions on Mobile Computing, vol. 24, no. 10, pp. 10 590–10 605, 2025

    2025

  11. [19]

    COMIX: Generalized conflict management in O-RAN xApps—architecture, workflow, and a power control case,

    A. E. Giannopoulos, S. T. Spantideas, G. Levis, A. S. Kalafatelis, and P. Trakadas, “COMIX: Generalized conflict management in O-RAN xApps—architecture, workflow, and a power control case,”IEEE Access, vol. 13, pp. 116 684–116 700, 2025

    2025

  12. [20]

    Conflict mitigation framework and conflict detection in O-RAN Near-RT RIC,

    C. Adamczyk and A. Kliks, “Conflict mitigation framework and conflict detection in O-RAN Near-RT RIC,”IEEE Communications Magazine, vol. 61, no. 12, pp. 199–205, 2023

    2023

  13. [21]

    QACM: QoS-aware xApp conflict mitigation in open RAN,

    A. Wadud, F. Golpayegani, and N. Afraz, “QACM: QoS-aware xApp conflict mitigation in open RAN,”IEEE Transactions on Green Com- munications and Networking, vol. 8, no. 3, pp. 978–993, 2024

    2024

  14. [22]

    ACCoRD: Actor-critic conflict resolution with deep learning for O-RAN xApps,

    C. Adamczyk and A. Kliks, “ACCoRD: Actor-critic conflict resolution with deep learning for O-RAN xApps,” inProc. IEEE INFOCOM Workshops, 2026, pp. 1–6

    2026

  15. [23]

    Open RAN conflict agents: Detecting and mitigating xApp conflicts with generative agents,

    D. C. Kwon and X. Zhang, “Open RAN conflict agents: Detecting and mitigating xApp conflicts with generative agents,” inProc. IEEE INFOCOM, 2026, pp. 1–10

    2026

  16. [24]

    Experimental evaluation of xApp conflict mitigation framework in O-RAN: Insights from testbed deployment in OTIC,

    A. Sultana, C. Adamczyk, M. Roy Chowdhury, A. Kliks, and A. Da Silva, “Experimental evaluation of xApp conflict mitigation framework in O-RAN: Insights from testbed deployment in OTIC,” in Proc. IEEE INFOCOM Workshops, 2025, pp. 1–6

    2025

  17. [25]

    Detecting out-of-order control messages in O-RAN: Dataset, benchmarks, and early-warning models,

    H. Gelban, R. Naim, and A. Badawy, “Detecting out-of-order control messages in O-RAN: Dataset, benchmarks, and early-warning models,” IEEE Open Journal of the Communications Society, vol. 7, pp. 1941– 1957, 2026

    1941

  18. [26]

    A runtime safety copilot for AI-native O-RAN: Predictive verification and fail-safe enforcement in Near-RT RIC control loops,

    M. A. Jawad, M. M. H. Munna, A. H. Kabir, N. H. Antu, and R. F. Tulona, “A runtime safety copilot for AI-native O-RAN: Predictive verification and fail-safe enforcement in Near-RT RIC control loops,” IEEE Access, vol. 14, pp. 63 106–63 120, 2026

    2026

  19. [27]

    Consistent updates for software-defined networks: Change you can believe in!

    M. Reitblatt, N. Foster, J. Rexford, and D. Walker, “Consistent updates for software-defined networks: Change you can believe in!” inProc. 10th ACM HotNets, 2011

    2011

  20. [28]

    Abstractions for network update,

    M. Reitblatt, N. Foster, J. Rexford, C. Schlesinger, and D. Walker, “Abstractions for network update,” inProc. ACM SIGCOMM, 2012, pp. 323–334

    2012

  21. [29]

    Dionysus: Dynamic scheduling of network updates,

    X. Jin, H. H. Liu, R. Gandhi, S. Kandula, R. Mahajanet al., “Dionysus: Dynamic scheduling of network updates,” inProc. ACM SIGCOMM, 2014, pp. 539–550

    2014

  22. [30]

    A NICE way to test OpenFlow applications,

    M. Canini, D. Venzano, P. Pere ˇs´ıni, D. Kosti´c, and J. Rexford, “A NICE way to test OpenFlow applications,” inProc. 9th USENIX NSDI, 2012, pp. 127–140

    2012

  23. [31]

    SDNRacer: Concurrency analysis for software-defined networks,

    A. El-Hassany, J. Miserez, P. Bielik, L. Vanbever, and M. Vechev, “SDNRacer: Concurrency analysis for software-defined networks,” in Proc. 37th ACM SIGPLAN PLDI, 2016, pp. 402–415

    2016

  24. [32]

    Abstraction-guided synthesis of synchronization,

    M. Vechev, E. Yahav, and G. Yorsh, “Abstraction-guided synthesis of synchronization,” inProc. 37th ACM SIGPLAN-SIGACT POPL, 2010, pp. 327–338

    2010

  25. [33]

    Synchronization synthesis for network programs,

    J. McClurg, H. Hojjat, and P. ˇCern´y, “Synchronization synthesis for network programs,” inProc. CAV, vol. 10427, 2017, pp. 301–321

    2017

  26. [34]

    Towards achieving energy efficiency and service availability in 6G O-RAN via formal verification,

    R. Metere, K. Ye, Y . Gu, Z. Zhang, D. Alrajehet al., “Towards achieving energy efficiency and service availability in 6G O-RAN via formal verification,” inProc. 12th Int. Symp. From Data to Models and Back (DataMod 2024), ser. Lecture Notes in Computer Science, vol. 15556, 20...

    2024

  27. [35]

    Agentic model checking,

    Y . Sun, J. Liu, D. Kroening, and J. Xue, “Agentic model checking,” 2026, arXiv:2605.21434

    2026 arXiv

  28. [36]

    Time, clocks, and the ordering of events in a distributed system,

    L. Lamport, “Time, clocks, and the ordering of events in a distributed system,”Communications of the ACM, vol. 21, no. 7, pp. 558–565, 1978

    1978

  29. [37]

    All from one, one for all: On model checking using repre- sentatives,

    D. Peled, “All from one, one for all: On model checking using repre- sentatives,” inProc. CAV, vol. 697, 1993, pp. 409–423

    1993

  30. [38]

    E. M. Clarke, O. Grumberg, and D. A. Peled,Model Checking. MIT Press, 1999

    1999

  31. [39]

    Godefroid,Partial-Order Methods for the Verification of Concurrent Systems

    P. Godefroid,Partial-Order Methods for the Verification of Concurrent Systems. Springer, 1996

    1996

  32. [40]

    Finding and reproducing heisenbugs in concurrent programs,

    M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainaret al., “Finding and reproducing heisenbugs in concurrent programs,” inProc. 8th USENIX OSDI, 2008, pp. 267–280

    2008

  33. [41]

    Dynamic partial-order reduction for model checking software,

    C. Flanagan and P. Godefroid, “Dynamic partial-order reduction for model checking software,” inProc. 32nd ACM SIGPLAN-SIGACT POPL, 2005, pp. 110–121

    2005

  34. [42]

    Optimal dynamic partial order reduction,

    P. A. Abdulla, S. Aronis, B. Jonsson, and K. Sagonas, “Optimal dynamic partial order reduction,” inProc. 41st ACM SIGPLAN-SIGACT POPL, 2014, pp. 373–384

    2014

  35. [43]

    Source sets: A foundation for optimal dynamic partial order reduction,

    ——, “Source sets: A foundation for optimal dynamic partial order reduction,”J. ACM, vol. 64, no. 4, pp. 25:1–25:49, 2017

    2017

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.