Pith. sign in

REVIEW 2 major objections 5 minor 38 references

An Abstract Domain for Heap Commutativity (Extended Version)

T0 review · 2 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read The paper proves that commutativity of concrete heap programs can be soundly decided by lifting them to an abstract domain of mathematical values, so that abstract commutativity conditions transfer back automatically as framed concrete…

desk verdict Good idea, clean examples, but the main theorem is overgeneralized and false as stated; the fix is to require H(Ψ+)=Prv(A). read the letter →

arxiv 2411.12857 v2 pith:A6BYTVHX submitted 2024-11-19 cs.PL cs.LO

Jared Pincus , Eric Koskinen This is my paper · ORCID
classification cs.PLcs.LO
keywords commutativityheap-manipulatingprogramsabstractinterpretationobservationalequivalenceseparationlogicprogramverificationGaloisconnectioncompositionalreasoning
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 proposes a way to prove that two heap-manipulating programs can be run in either order with the same observable result. The idea is to lift each heap data structure to a simpler mathematical value—a list for a stack, a set for an unordered collection, an integer for a counter—and do the commutativity reasoning there, where it is far easier. The paper's main theorem says that a commutativity condition found for the abstract functions transfers soundly back to the concrete heap programs, and the transferred condition is automatically framed so it also holds in any larger heap. The authors demonstrate the pattern on several data structures and mechanize the theory in an interactive proof assistant.

What carries the argument

The central object is the abstract domain $\mathcal{A}_A = X + \{\bot,\top,\mathsf{\times},\mathsf{\checkmark}\}$, built from a set of abstract values $X$ and a projection $\pi$ from concrete heaps to $X$ or the special out-of-purview value $\mathsf{\times}$. The projection satisfies a locality constraint, and together with the concretization function it forms a Galois connection to the concrete heap powerset. Abstract programs are transformers over this domain, a soundness relation connects them to concrete programs, and abstract commutativity is defined by requiring both orders to yield the same in-purview abstract value. Theorem 1 carries the reduction by threading an abstract commutativity condition through the projection into a concrete condition on heaps.

What would settle it

Exhibit a concrete Himp program $f$ and a heap $h+h'$ where $f$ reads or writes an address outside its stated footprint, so that Definition 2(3) fails; then Theorem 1 is inapplicable, and a derived commutativity condition would be observed to fail on that larger heap if the program were nonetheless passed through the abstraction.

Watch

Extended reading notes

Core claim

The central claim is Theorem 1: if an abstract program $m$ soundly abstracts a concrete program $f$, $n$ soundly abstracts $g$, the abstract programs commute under condition $Q$, and the abstraction $A$ captures the observational equivalence $[\Psi,\sim]$, then the concrete programs $f$ and $g$ commute under the derived condition $P^+$, where $P(h)$ requires $\pi_A(h)\in X_A$ and $Q(\pi_A(h))$. Sound abstraction means the abstract program over-approximates the concrete behavior and also fails when the concrete program fails on an in-purview heap. Thus a user can replace heap programs by functions over mathematical values, reason about commutativity there, and automatically obtain a framed, separation-logic-style precondition for the original heap code.

Load-bearing premise

Every concrete program under analysis must be a total function that terminates or fails in finite time and acts locally, touching nothing outside its footprint; the paper lifts its example language to this model but does not formalize that lifting.

Editorial extensions

If this is right

  • A verification engineer can check commutativity of concrete push and pop by reasoning about list append and remove; the concrete separation-logic precondition is derived automatically.
  • The derived concrete conditions are framed: if two heap programs commute on a small heap, the same condition also holds when a disjoint heap is added.
  • Composition of abstract domains mirrors separating conjunction, so commutativity results about separate data structures can be combined, as illustrated by a stack with a size counter.
  • The soundness conditions—termination, local action, and failure preservation—delimit exactly which concrete programs the technique covers.
  • The same abstract domain supports both verification-style soundness proofs and synthesis-style abstract commutativity conditions, so existing synthesis techniques can be aimed at the abstract functions rather than at pointer layouts.

Reading between the lines

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

  • The projection-and-transfer scheme should apply to other binary relations over heaps, such as refinement or observational equivalence, not only to commutativity.
  • Because the abstract space is finite or otherwise simpler than the heap space, an automated counterexample-guided synthesis loop over abstract programs would likely yield heap commutativity conditions without symbolic execution over pointer layouts; the paper leaves this automation to future work.
  • The locality constraint on projections is not just a convenience: it is what makes the composition $A*B$ well-defined, so relaxing it would require a new uniqueness argument for composed abstractions.
  • A practical tool built on this theory would need to handle programs that read or write outside their footprint, or that diverge; those programs fall outside the theorem's guarantee and could be treated by a separate analysis.
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

2 major / 5 minor

Summary. The paper introduces an abstract domain for heap commutativity. It builds an abstraction A=(X,pi) with a projection pi from heaps to abstract values plus special elements (cross, check, bottom, top), defines abstract programs and a soundness relation m↝_A f, and proves a sound commutativity theorem that derives a framed concrete commutativity condition from abstract commutativity. It then introduces composition of abstract domains and programs, with noninterference and compositional commutativity results, and applies the framework to a counter, a two-set, a linked-list stack, and a combined stack/counter. The authors state that the core theory is mechanized in Coq, with the Himp example semantics excluded.

Significance. If the main theorem is repaired, the paper offers a genuinely useful reduction: heap commutativity obligations can be discharged by reasoning on simple mathematical structures, with framing and composition built in. The compositional operators in Section 6 and the worked examples give concrete evidence of applicability. The claimed Coq mechanization of the general semantics and of the uniqueness/well-definedness proofs is a strength, though the artifact is not inspectable from the text and the Himp examples are outside the mechanized core. Because Theorem 1 is false as printed, the paper is not yet acceptable, but the identified gaps appear fixable within the paper's scope.

major comments (2)
  1. [§5.2, Def. 12, Thm. 1] The central soundness theorem is false as stated. Definition 12 only requires H(Ψ+)⊆Prv(A), while the conclusion's condition P+ ranges over all heaps with a purview subheap and requires outputs to lie in H(Ψ+). Counterexample: take X={∗}, π(h)=∗ for all h, Ψ=1↦0, ∼ universal on H(Ψ+), f=g=id, m=n=x↦∗, and Q=⊤. Then A captures [Ψ,∼], m and n are sound, and m⊲⊳^⊤_A n, but the empty heap satisfies P+ while (id;id)(∅)={∅} and ∅∉H(Ψ+), so no h′∈H(Ψ+) can have {∅}⊆[h′]∼. Requiring H(Ψ+)=Prv(A) is not sufficient by itself: with Ψ defined as a↦0, π(h)=0 iff a∈dom(h), ∼ equal to equality of the a-value, f(h)=h[a:=0], g(h)=h[a:=1] on the domain where a is defined, and m=n=x↦0, all hypotheses (including H(Ψ+)=Prv(A)) hold, yet f;g and g;f produce different a-values, so the union of outputs is not contained in one ∼-class. The theorem therefore needs either to be stated for [Prv(A),∼A] (the form used in all examples) or to strengthen Definition 12 so that π-equality implies ∼ on all of H(Ψ+), not only on H(Ψ). This is load-bearing because Theorem 1 underlies the derived conditions in Sections 5 and 7.
  2. [§3.3 and §7] The bridge from Himp programs to the concrete programs of Definition 2 is not formalized. Section 3.3 states that Himp has not been formalized in Coq and that Himp programs are implicitly lifted to those concrete programs, but the lifting proof is not given. The soundness and capture facts for the worked examples are only asserted via symbolic execution in Section 7, so the advertised example-level concrete conditions are not part of the mechanized core. The paper should either formalize the Himp semantics and the locality/lifting proofs, or state explicitly in the conclusions and limitations that the example-level soundness and capture facts are unverified outside the Coq development.
minor comments (5)
  1. [Def. 4 and Def. 7] The letter A is overloaded: it denotes both the pair ⟨X,π⟩ and the full lattice X+⊥+⊤+✗+✓, as in 'm : X→A' and 'A∗B'. Please disambiguate these two uses.
  2. [§7.1, table] In the table for the non-negative counter, the row for incr_p and read_r^p lists P=⊥; since P is a heap predicate, please clarify that this denotes the false predicate rather than the abstract bottom.
  3. [§9] The conclusion says all theorems, lemmas, and examples have been mechanized in Coq, but Section 3.3 excludes the Himp concrete semantics; please make this exclusion explicit in the conclusion and abstract.
  4. [Supplement] The text says the Coq development is available in the supplement, but no artifact identifier or repository link is given, which makes it impossible for a reader to verify the mechanization claims from the arXiv text alone.
  5. [Def. 12] The observation that A always captures [Prv(A),∼A] relies on locality to obtain H(Prv(A)+)=Prv(A), but this equality is not stated explicitly; making it explicit would clarify the condition that Theorem 1 actually needs.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the abstract commutativity condition is an independent input and the concrete condition is derived by a mechanized soundness theorem, not by construction.

full rationale

The central derivation is Theorem 1: concrete commutativity f ⊲⊳^P+_[Ψ,∼] g follows from abstract commutativity m ⋈^Q_A n, per-program soundness m↝_A f and n↝_A g, and the capture hypothesis. The abstract condition Q is chosen or synthesized in the abstract space independently of the target concrete commutativity conclusion; the derived concrete condition P(h) ≡ πA(h)∈XA ∧ Q(πA(h)) is a consequence of these inputs, not an input itself. Definition 8 is a standard abstract-interpretation soundness requirement (over-approximation plus failure propagation), not a restatement of commutativity, and it is proved for each example by symbolic execution. The example concrete conditions are obtained by applying the theorem after those soundness proofs, so they are not fitted to the target result. The only self-citations, such as the authors' earlier synthesis work and Pincus's preliminary thesis, are used for context or as pointers to automation-oriented prior work; they are not load-bearing premises, no uniqueness theorem is imported from them, and no ansatz is smuggled in by citation. The paper explicitly notes that Himp itself has not been formalized in Coq and that concrete example programs are implicitly lifted from its semantics; this is a real completeness/soundness limitation but not a circularity. The skeptical counterexample to Theorem 1 as stated concerns whether Definition 12's one-way inclusion H(Ψ+)⊆Prv(A) is sufficient for the conclusion; that is a potential soundness bug in the theorem statement, not a reduction of the conclusion to its own assumptions. Overall, no circular step is identifiable from the paper's equations or citation chain.

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

The central claim rests on formal modeling choices rather than fitted quantities. The paper introduces two internal constructs, the abstract value markers and the composition operator, that are justified by the formal development, not by external evidence. No free parameters are fitted to data.

assumptions (5)
  • domain assumption Concrete programs are total functions f: H -> P(H) that terminate or fail in finite time and act locally (Def. 2).
    The soundness theorem is stated for this program model; Section 3.3 lifts Himp programs to it informally. A program that violates local action falls outside the theorem's scope.
  • domain assumption Every projection pi satisfies locality: for disjoint h,h', pi(h) in X implies pi(h+h') = pi(h) (Def. 4).
    This is what makes derived commutativity conditions framed and guarantees uniqueness in the composition A*B (Def. 13). Users must choose abstractions with this property.
  • domain assumption Heaps are finite partial maps and there are always fresh addresses available for allocation (Sec. 3.1).
    Used throughout for nondeterministic allocation and for the finite-footprint reasoning in Def. 2.
  • standard math The abstract domain A_A with the specified partial order is a complete lattice (Def. 4).
    Needed to form joins in the abstraction function alpha and to have a well-defined Galois connection.
  • standard math The Separation Logic Foundations library used for the Coq development is sound.
    Stated as the basis for the mechanization in the Supplement paragraph; the paper assumes the library's definitions and lemmas.
invented entities (2)
  • Abstract markers ✗, ✓, ⊥, ⊤
    purpose: Extend the set of abstract values into a complete lattice so that out-of-purview heaps, ambiguity, failure, and arbitrary heaps have denotations in the Galois connection.
    Formal devices internal to the theory; no experimental prediction is attached to them.
  • Abstract domain composition A*B and abstract program composition m*n
    purpose: Mirror separating conjunction on concrete heaps and enable compositional commutativity results for multiple data structures and method arguments.
    Mathematical constructions validated by the paper's own theorems (Def. 13-15, Thm. 3-4); they do not come with an external falsifiable handle.

how reviews work

0 comments
Cite this review

Pith. "Pith review of An Abstract Domain for Heap Commutativity (Extended Version)." pith.science (2026). https://pith.science/paper/A6BYTVHX

@misc{pith2026241112857,
  author       = {Pith},
  title        = {Pith review of: An Abstract Domain for Heap Commutativity (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/A6BYTVHX}},
  note         = {Machine review of arXiv:2411.12857}
}
read the original abstract

Commutativity of program code (i.e. the equivalence of two code fragments composed in alternate orders) is of ongoing interest in many settings such as program verification, scalable concurrency, and security analysis. While some have explored static analysis for code commutativity, few have specifically catered to heap-manipulating programs. We introduce an abstract domain in which commutativity synthesis or verification techniques can safely be performed on abstract mathematical models and, from those results, one can directly obtain commutativity conditions for concrete heap programs. This approach offloads challenges of concrete heap reasoning into the simpler abstract space. We show this reasoning supports framing and composition, and conclude with commutativity analysis of programs operating on example heap data structures. Our work has been mechanized in Coq and is available in the supplement.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

38 extracted references · 25 canonical work pages

  1. [1]

    Antonopoulos, T., Koskinen, E., Le, T.C., Nagasamudram, R., Naumann, D.A., Ngo, M.: An algebra of alignment for relational verification . Proc. ACM Program. Lang. 7(POPL), 573–603 (2023). https://doi.org/10.1145/357121 3

    work page doi:10.1145/357121 2023

  2. [2]

    Automatic Generation of Precise and Useful Commutativity Conditions (Extended Version)

    Bansal, K., Koskinen, E., Tripp, O.: Automatic generatio n of precise and useful commutativity conditions (extended version). C oRR (2018), http://arxiv.org/abs/1802.08748

    work page Pith review arXiv 2018

  3. [3]

    Bansal, K., Koskinen, E., Tripp, O.: Synthesizing precis e and useful commutativity conditions. J. Autom. Reason. 64(7), 1333–1359 (2020). https://doi.org/10.1007/S10817-020-09573-W

    work page doi:10.1007/s10817-020-09573-w 2020

  4. [4]

    In: 22nd Annual IEEE Symposium on Logic in Computer Science ( LICS 2007)

    Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and ab stract separation logic. In: 22nd Annual IEEE Symposium on Logic in Computer Science ( LICS 2007). pp. 366–378 (2007). https://doi.org/10.1109/LICS.2007.30

    work page doi:10.1109/lics.2007.30 2007

  5. [5]

    Charguéraud, A.: Separation Logic Foundations, Softwar e Foundations, vol. 6. Electronic textbook (2023), http://softwarefoundations .cis.upenn.edu, version 2.0

    work page 2023

  6. [6]

    Chen, A., Fathololumi, P., Koskinen, E., Pincus, J.: Vera city: Declarative multicore programming with commutativity. Proc. ACM Program. Lang. 6(OOPSLA2) (oct 2022). https://doi.org/10.1145/3563349

    work page doi:10.1145/3563349 2022

  7. [7]

    In: André, É., Sun, J

    Chen, A., Fathololumi, P., Nicola, M., Pincus, J., Brenna n, T., Koskinen, E.: Bet- ter predicates and heuristics for improved commutativity s ynthesis. In: André, É., Sun, J. (eds.) Automated Technology for Verification and Ana lysis - 21st Interna- tional Symposium, ATV A 2023, Singapore, October 24-27, 202 3, Proceedings, Part II. Lecture Notes in Compu...

    work page doi:10.1007/978-3-031-45332-8_5 2023

  8. [8]

    In: Proceedings of the Twenty-Fourth ACM Symposium on Opera ting Systems Principles

    Clements, A.T., Kaashoek, M.F., Zeldovich, N., Morris, R .T., Kohler, E.: The scalable commutativity rule: Designing scalable software for multicore processors. In: Proceedings of the Twenty-Fourth ACM Symposium on Opera ting Systems Principles. pp. 1–17. SOSP ’13, Association for Computing M achinery, New York, NY, USA (2013). https://doi.org/10.1145/251...

    arXiv 2013

Show all 38 references
  1. [9]

    Electronic Proceedings in Theoretical Co mputer Science 129, 325– 336 (sep 2013)

    Cortesi, A., Costantini, G., Ferrara, P.: A survey on prod uct operators in abstract interpretation. Electronic Proceedings in Theoretical Co mputer Science 129, 325– 336 (sep 2013). https://doi.org/10.4204/eptcs.129.19

    2013 doi

  2. [10]

    In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Pro gramming Languages

    Cousot, P., Cousot, R.: Abstract interpretation: A unifi ed lattice model for static analysis of programs by construction or approximation of fix points. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Pro gramming Languages. pp. 238–252. POPL ’77, Assoc...

    1977 doi

  3. [11]

    The Journal of Logic Programming 13(2), 103–179 (1992)

    Cousot, P., Cousot, R.: Abstract interpretation and app lication to logic programs. The Journal of Logic Programming 13(2), 103–179 (1992). https://doi.org/10.1016/0743-1066(92)90030-7

    1992 doi

  4. [12]

    In: Proceedings of the ACM Symposium on Pri nciples of Dis- tributed Computing

    Dickerson, T., Gazzillo, P., Herlihy, M., Koskinen, E.: Adding concurrency to smart contracts. In: Proceedings of the ACM Symposium on Pri nciples of Dis- tributed Computing. pp. 303–312. PODC ’17, ACM, New York, NY , USA (2017). https://doi.org/10.1145/3087801.3087835

    2017

  5. [13]

    Eilers, M., Dardinier, T., Müller, P.: Commcsl: Proving information flow security for concurrent programs using abstract commutativity. Pro c. ACM Program. Lang. 7(PLDI), 1682–1707 (2023). https://doi.org/10.1145/3591 289

    2023 doi

  6. [14]

    ACM SIGPLAN Notices 44(1), 2–15 (2009) 22 J

    Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic a ctions. ACM SIGPLAN Notices 44(1), 2–15 (2009) 22 J. Pincus and E. Koskinen

    2009

  7. [15]

    Enea, C., Koskinen, E.: Scenario-based proofs for concu rrent objects. Proc. ACM Program. Lang. (to appear) (OOPSLA2) (2024)

    2024

  8. [16]

    In : LICS

    Farzan, A.: Commutativity in automated verification. In : LICS. pp. 1–7 (2023). https://doi.org/10.1109/LICS56636.2023.10175734

    2023

  9. [17]

    Farzan, A., Klumpp, D., Podelski, A.: Stratified commuta tivity in verification algo- rithms for concurrent programs. Proc. ACM Program. Lang. 7(POPL), 1426–1453 (2023). https://doi.org/10.1145/3571242

    2023 doi

  10. [18]

    Farzan, A., Klumpp, D., Podelski, A.: Commutativity sim plifies proofs of param- eterized programs. Proc. ACM Program. Lang. (POPL) (2024)

    2024

  11. [19]

    Farzan, A., Mathur, U.: Coarser equivalences for causal concurrency. Proc. ACM Program. Lang. 8(POPL), 911–941 (2024). https://doi.org/10.1145/363287 3

    2024 doi

  12. [20]

    Proceedings of the ACM on Programming Languages 4(OOPSLA), 1–29 (2020)

    Flanagan, C., Freund, S.N.: The anchor verifier for block ing and non-blocking concurrent software. Proceedings of the ACM on Programming Languages 4(OOPSLA), 1–29 (2020)

    2020

  13. [21]

    Theoretical Computer Science 216(1), 159–211 (1999)

    Giacobazzi, R., Ranzato, F.: The reduced relative power operation on abstract domains. Theoretical Computer Science 216(1), 159–211 (1999). https://doi.org/10.1016/S0304-3975(98)00194-7

    1999 doi

  14. [22]

    ACM Trans

    Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstr act domains condensing. ACM Trans. Comput. Logic 6(1), 33–60 (Jan 2005). https://doi.org/10.1145/1042038.1042040

    2005

  15. [23]

    ACM Trans

    Giacobazzi, R., Scozzari, F.: A logical model for relati onal abstract do- mains. ACM Trans. Program. Lang. Syst. 20(5), 1067–1109 (Sep 1998). https://doi.org/10.1145/293677.293680

    1998

  16. [24]

    In: Proceedi ngs of the 32nd ACM SIGPLAN Conference on Programming Language Design and Impl ementation

    Kim, D., Rinard, M.C.: Verification of semantic commutat ivity conditions and inverse operations on linked data structures. In: Proceedi ngs of the 32nd ACM SIGPLAN Conference on Programming Language Design and Impl ementation. pp. 528–541. PLDI ’11, Association for Computing M...

    2011

  17. [25]

    In: International Conference on Verificat ion, Model Checking, and Abstract Interpretation

    Koskinen, E., Bansal, K.: Decomposing data structure co mmutativity proofs with mn-differencing. In: International Conference on Verificat ion, Model Checking, and Abstract Interpretation. pp. 81–103. Springer (2021)

    2021

  18. [26]

    In: 2021 Formal M ethods in Computer Aided Design (FMCAD)

    Kragl, B., Qadeer, S.: The CIVL verifier. In: 2021 Formal M ethods in Computer Aided Design (FMCAD). pp. 143–152. IEEE (2021)

    2021

  19. [27]

    In: Enea, C., Lal, A

    Lette, D., Farzan, A.: Commutativity for concurrent pro gram termination proofs. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35t h International Conference, CA V 2023, Paris, France, July 17-22, 2023, Proc eedings, Part I. Lecture Notes in Computer Science, vol. ...

    2023 doi

  20. [28]

    In: 36th Annual ACM/IEEE Symposium on Logic in Compu ter Sci- ence, LICS 2021, Rome, Italy, June 29 - July 2, 2021

    Nagasamudram, R., Naumann, D.A.: Alignment completene ss for relational hoare logics. In: 36th Annual ACM/IEEE Symposium on Logic in Compu ter Sci- ence, LICS 2021, Rome, Italy, June 29 - July 2, 2021. pp. 1–13. IEEE (2021). https://doi.org/10.1109/LICS52264.2021.9470690

    2021

  21. [29]

    In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of pr ogramming languages

    Parkinson, M., Bierman, G.: Separation logic and abstra ction. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of pr ogramming languages. pp. 247–258 (2005)

    2005

  22. [30]

    Maste r’s thesis, Stevens Insti- tute of Technology (2022), https://www.proquest.com/doc view/2681771819

    Pincus, J.: Commutativity Reasoning for the Heap. Maste r’s thesis, Stevens Insti- tute of Technology (2022), https://www.proquest.com/doc view/2681771819

    2022

  23. [31]

    1327–1341

    Pîrlea, G., Kumar, A., Sergey, I.: Practical Smart Contr act Sharding with Own- ership and Commutativity Analysis, pp. 1327–1341. Associa tion for Computing Machinery, New York, NY, USA (2021), https://doi.org/10.1 145/3453483.3454112 An Abstract Domain for Heap Commutativity 23

    2021

  24. [32]

    In: Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and i mplementation

    Prabhu, P., Ghosh, S., Zhang, Y., Johnson, N.P., August, D.I.: Commutative set: A language extension for implicit parallel programming. In: Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and i mplementation. pp. 1–11 (2011). https://doi.org/10.11...

    2011

  25. [33]

    In: Pro- ceedings 17th Annual IEEE Symposium on Logic in Computer Sci ence

    Reynolds, J.: Separation logic: a logic for shared mutab le data structures. In: Pro- ceedings 17th Annual IEEE Symposium on Logic in Computer Sci ence. pp. 55–74 (2002). https://doi.org/10.1109/LICS.2002.1029817

    2002 arXiv

  26. [34]

    In: Euro-Par ’96 Parallel Processing, Second International Eu ro-Par Conference, Lyon, France, August 26-29, 1996, Proceedings, Volume I

    Rinard, M.C., Diniz, P.C.: Semantic foundations of comm utativity analysis. In: Euro-Par ’96 Parallel Processing, Second International Eu ro-Par Conference, Lyon, France, August 26-29, 1996, Proceedings, Volume I. pp . 414–423 (1996). https://doi.org/10.1007/3-540-61626-8_55

    1996 doi

  27. [35]

    Shapiro, M., Preguiça, N., Baquero, C., Zawirski, M.: A c omprehensive study of convergent and commutative replicated data types. Ph.D. thesis, Inria–Centre Paris-Rocquencourt; INRIA (2011)

    2011

  28. [36]

    In: Proceedings of the 1st International Workshop on Emerging Applications of Abs tract Interpretation (EAAI06)

    Sims, E.J.: An abstract domain for separation logic form ulae. In: Proceedings of the 1st International Workshop on Emerging Applications of Abs tract Interpretation (EAAI06). pp. 133–148. ENTCS, Vienna, Austria (2006)

    2006

  29. [37]

    In: Proceedings of the second annual ACM symposium on Principles of distributed computing (PODC’83)

    Weihl, W.E.: Data-dependent concurrency control and re covery (extended ab- stract). In: Proceedings of the second annual ACM symposium on Principles of distributed computing (PODC’83). pp. 63–75. ACM Press, New York, NY, USA (1983). https://doi.org/10.1145/800221.806710

    1983

  30. [38]

    Yang, H.: Relational separation logic. Theor. Comput. S ci. 375(1-3), 308–334 (2007). https://doi.org/10.1016/J.TCS.2006.12.036 Appendix To share a specific example of isomorphism, as well as an alter native way to construct abstract domains, we return to our two-set exampl e (...

    2007 doi

Pith tools

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