Pith. sign in

REVIEW 3 major objections 5 minor 29 references

Automatic Inference of Relational Object Invariants

T0 review · 3 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 shows that isolating the most recently used object in a per-bank cache lets an abstract interpreter infer relational object invariants such as buffer length not exceeding capacity, and that the resulting domain outperforms the…

desk verdict The MRU-cache idea is good and the evaluation is solid, but the printed cacheSync equations have the used flag inverted, which breaks the soundness argument as written. read the letter →

arxiv 2411.14735 v1 pith:Q2RVQPFP submitted 2024-11-22 cs.PL

Yusen Su , Jorge A. Navas , Arie Gurfinkel , Isabel Garcia-Contreras This is my paper · ORCID
classification cs.PL MSC 68Q60
keywords objectinvariantsabstractinterpretationrecent-usememorymodelMRUabstractionheapsummarizationstrongupdatesrelationalanalysisstatic
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

The paper tries to establish that relational object invariants—properties like a buffer's length never exceeding its capacity—can be inferred automatically by an abstract interpreter that separates, within each memory region, the single most recently used object from all other objects summarized together. Because the most recently used object is represented exactly, field updates to it are strong updates, so temporary violations of an invariant during a multi-field update never pollute the summarized invariants for the rest of the objects. The paper backs this with a new memory model (RUMM) that gives every memory bank a one-slot cache for the MRU object, and a composite abstract domain (MRUD) that combines numerical domains with lightweight equality information to propagate facts between the cache and the scalar state. If the approach is right, analyses can prove assertions in small C programs that recency-based and summarization-based domains cannot, and they can do so with a 76x average speedup over the existing summarization domain in the same abstract interpreter.

What carries the argument

The load-bearing mechanism is the pair of operations pack♯ and unpack♯, driven by the cacheSync♯ function on every load or store. When a dereferenced pointer does not alias the cached object, cacheSync♯ flushes the dirty cache into the bank's summary object (pack♯), copies the summary into the cache as the new MRU object (unpack♯), and records the pointer-equality cachebase ≈ ptrbase in the equality domain. This isolates every field update to the single concrete object, so numerical invariants like len <= cap are maintained in the summary even while the cached object is temporarily out of invariant. A bidirectional domain reduction uses the field-scalar equalities (e.g., len ≈ i and cap ≈ sz) to refine the cache from scalar facts and vice versa, which is what lets the analysis discover the relational invariant in the first place.

What would settle it

Run the analysis on a set of programs whose memory safety is independently checked by a bounded model checker with a large unwinding bound; any assertion that the analysis proves safe but the checker finds a counterexample for would refute the central claim. More directly, search for a program whose reachable states under the recent-use memory model differ from those under the standard C memory model—for example, via an aliased write that a cache flush overwrites in one model but not the other.

Watch

Extended reading notes

Core claim

The central discovery is that recency of use, not recency of allocation, is the right axis for precise heap abstraction. The paper defines RUMM, in which memory is partitioned into banks, each bank holds its objects in a storage region and has a cache that contains at most one object—the most recently used one. All accesses go through the cache: on a miss, the current cache object is 'packed' back into the summary that stands for all objects in the bank, and the newly addressed object is 'unpacked' from that summary. Because the cache holds a single concrete object, writes to it are strong updates that cannot weaken the summary's invariants. The resulting MRUD abstract domain, a reduced product of numerical and equality sub-domains over scalars and fields, therefore infers object invariants such as len <= cap that are broken transiently during a series of field updates, and the evaluation shows it proves all assertions in a small benchmark suite while outperforming the prior summarization domain by two orders of magnitude on average run time.

Load-bearing premise

The load-bearing premise is that the recent-use memory model, with its per-bank cache and storage, faithfully preserves all reachable states of the standard C memory model, so that invariants proved under RUMM transfer to the real program.

Editorial extensions

If this is right

  • Assertions that require relational object invariants—like the len <= cap check that recency-based and prior summarization-based analyses both fail to prove—become provable in the same abstract-interpretation pipeline.
  • Pre-processing with the new domain can discharge a majority of memory-safety assertions before loop unrolling, reducing the work left for a bounded model checker and cutting end-to-end verification time in the majority of evaluated tasks.
  • The composite design makes the analysis scalable: because each memory bank is represented by small separate difference-bound matrices, joins are cheap, and the domain reports on average a 76x speedup (up to 81x without reduction) over the single-DBM summarization domain on 114 programs.
  • The technique is parameterized by numerical domain, so it can be instantiated with Zones, Octagons, or richer domains; the observed precision limits are tied to the expressiveness of those domains and to unsupported string-length tracking.

Reading between the lines

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

  • The MRU/cache idea could be applied to other clients besides object invariants, such as typestate or shape properties, by choosing a different abstract domain for the cache and the summary; the pack/unpack discipline is largely domain-agnostic.
  • The claimed compatibility between RUMM and the standard C memory model suggests that a mechanized bisimulation proof would be a natural next step, since the paper's soundness argument is asserted rather than fully demonstrated.
  • Precision could likely be improved beyond the reported results by making the summary non-uniform—for example, by also partitioning summarized objects by recency of allocation, which the paper hints at as a possible combination with extensions of recency abstraction.
  • The reported speedup is measured with Zones/Octagons and a heuristic reduction strategy, so a reader should expect different ratios with polyhedral or non-relational numerical domains.
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

3 major / 5 minor

Summary. The paper introduces RUMM, a concrete memory model that partitions memory into banks and gives each bank an MRU cache, and MRUD, an abstract domain that represents the cached object exactly while summarizing the rest of the bank. The intended contribution is to enable strong updates to the active object without weakening summarized invariants, thereby inferring relational object invariants such as length <= capacity. The paper defines concrete and abstract transfer functions, a reduction procedure, an implementation in Crab, and an experimental comparison against Crab's summarization domain, Mopsa with recency, and a bounded-model-checking pipeline. The central claim is that MRUD is both more precise and dramatically more scalable than the state of the art.

Significance. If the approach were sound, it would be a valuable contribution to heap abstraction for relational properties: the MRU-cache idea is a natural extension of recency abstraction, and the modular composite domain design is plausible for scalability. The paper provides a public implementation and benchmarks, which is a strength. However, the central claim depends on the correctness of the RUMM semantics and of the MRUD abstraction; the manuscript does not provide a soundness proof, and the formal semantics as printed is internally inconsistent with the paper's own motivating example.

major comments (3)
  1. [Section 3, Fig. 6 (and Fig. 11)] The guard of cacheSync in Fig. 6 is `¬used ∧ ptrbase ≠ cachebase`. Since Section 3 defines `used` as 'indicating the cache is active', the guard is false for every access after the first one (once `used` becomes `true`), so the cache is never flushed or refreshed on a miss. This contradicts the execution shown in Fig. 4b, where a second object is loaded into the cache even though `used` is `true` at step (1). Concretely, the trace `store(&A,len,1); store(&B,len,2)` leaves `B` untouched and writes `A.len=2`. The abstract `cacheSync♯` in Fig. 11 inherits the same inverted condition, so the analysis can update a stale cached object and discharge assertions about the wrong object (e.g., the Fig. 1 example would update the obsolete `p` object rather than `ary[0]`). This is a load-bearing error: it breaks the claimed bisimulation in Section 3 and the soundness of the abstract semantics.
  2. [Section 4, soundness paragraph] The paper explicitly omits the soundness proof of the abstract semantics ('We omit it here since the abstraction is straightforward') and only asserts the bisimulation between RUMM and CMM via two informal reasons in Section 3. Given that the concrete semantics as printed is incorrect (previous comment), the omitted proof cannot be treated as a routine detail. The authors need to provide a rigorous bisimulation proof for RUMM vs CMM and a soundness or Galois-connection argument for the MRUD abstraction, covering the pack/unpack and flushCache operations. Without this, the experimental claims in Section 6 do not establish that the tool proves true assertions.
  3. [Appendix A, Fig. 19] The helper `flushCache♯` returns `mb` unchanged when `used` is true. Since the domain operations (Fig. 18) call `flushCache♯` specifically to clear each bank's cache before the pairwise lattice operations, the cache remains dirty and active during joins and widening, contrary to the intended semantics described in the text. This is another instance of the inverted `used` condition and should be corrected together with `cacheSync` and `cacheSync♯`.
minor comments (5)
  1. [Fig. 12 caption] The caption contains a typo: 'after the first iteration opf the loop' should read 'of the loop'.
  2. [Abstract vs. Section 6] The abstract reports a '75X faster' speedup, while Section 6 reports an average of '76x' for the OPT configuration; these numbers should be made consistent.
  3. [Sections 4 and 5] The text refers to 'the extended version of the paper' for the full domain operations and the equality domain details, but no link or reference is given for that version; the material should be included or clearly referenced.
  4. [Table 1] The column headers 'safe warn safe warn' make it difficult to tell which domain each pair of columns belongs to; a clearer layout is needed.
  5. [Section 1, paragraph on Mopsa] The sentence 'Mopsa with recency does not prove the assertion on line 20, since the inferred invariant is len >0 ∧ cap >1' is confusing because the invariant does not imply len <= cap; it would be clearer to state explicitly that the inferred invariant is too weak to prove the assertion.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: RUMM/MRUD is defined from its own concrete semantics and evaluated on external benchmarks; self-citations are infrastructural, not load-bearing.

full rationale

The derivation chain is self-contained. Section 3 defines RUMM concretely (Figs. 5-6) and Section 4 derives the abstract transfer functions from that concrete semantics (Figs. 10-11); no parameter is fitted to the benchmarks and no result is defined in terms of the target invariant. The scalability claim is measured on 114 programs including GNU Coreutils, and the case study uses AWS-based tasks, so the headline results are not forced by construction. The paper cites the authors' own CRAB [14] and SeaBMC [26], but only as implementation infrastructure and comparison baseline, not as justification for the central semantic claim. The 7 precision benchmarks are authored by the same group and mirror the motivating examples, but they are used as test inputs, not as fitted data; this is at most a weak evaluation-selection concern, not circularity. The paper explicitly omits the soundness proof ("We omit it here since the abstraction is straightforward", Section 4) and asserts rather than proves a bisimulation between RUMM and CMM (Section 3); these are missing-support/correctness gaps, not circular reductions. A separate noted inconsistency in Fig. 6's cacheSync guard (`\neg used \land ptrbase \neq cachebase`) would, if real, be a soundness bug in the printed semantics, but it does not make the derivation circular.

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

The central claim rests on the RUMM memory model, the MRUD composite domain, and the soundness of the pack/unpack abstraction. The paper omits the soundness proof for the abstraction and the bisimulation argument is informal. No numeric parameters are fitted to data; the only free choices are design heuristics (e.g., OPT reduction strategy) and benchmark selection.

assumptions (5)
  • standard math Abstract interpretation framework and standard numeric domains (Zones/Octagons) are sound.
    The paper relies on standard abstract interpretation theory, Galois connections, and DBM-based numeric domains (Sections 2 and 4).
  • domain assumption CrabIR is an adequate IR and the C-to-CrabIR compilation with SeaDsa preserves the relevant heap structure.
    Used throughout the implementation (Section 5); the analysis operates on CrabIR, and bank partitioning depends on SeaDsa allocation-site results.
  • ad hoc to paper RUMM is bisimilar to the standard C memory model.
    Stated in Section 3 with a two-point argument, no proof given; this underpins transfer of results from the analysis to the original program.
  • ad hoc to paper The abstract pack/unpack operations soundly approximate concrete flush/refresh.
    Section 4 defines pack/unpack and says soundness follows from the abstraction and Galois connections, but the proof is omitted.
  • domain assumption Heap objects in the same memory bank can be merged into one summary object without losing the invariants of interest.
    This is the summarization step in Section 4; precision results depend on it, and the paper gives no formal precision guarantee.
invented entities (3)
  • Recent-use memory model (RUMM) with per-bank cache and storage
    purpose: To separate the most recently used object from summarized objects so field updates can be strong.
    RUMM is a new formal memory model introduced in Section 3. It is an internal abstraction, not an independently observable entity; its only validation is the paper's experiments.
  • MRUD abstract domain (reduced product with equality domains)
    purpose: To represent object invariants scalably and propagate equalities between scalars and object fields.
    Defined in Section 4; it is a new analysis construct. No external falsifiable handle beyond the reported benchmarks.
  • MRU cache and summary object with pack/unpack operations
    purpose: To maintain a precise singleton (cache) and a merged invariant (summary) during analysis.
    These are auxiliary abstractions inside MRUD; their correctness is part of the omitted soundness proof.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Automatic Inference of Relational Object Invariants." pith.science (2026). https://pith.science/paper/Q2RVQPFP

@misc{pith2026241114735,
  author       = {Pith},
  title        = {Pith review of: Automatic Inference of Relational Object Invariants},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/Q2RVQPFP}},
  note         = {Machine review of arXiv:2411.14735}
}
read the original abstract

Relational object invariants (or representation invariants) are relational properties held by the fields of a (memory) object throughout its lifetime. For example, the length of a buffer never exceeds its capacity. Automatic inference of these invariants is particularly challenging because they are often broken temporarily during field updates. In this paper, we present an Abstract Interpretation-based solution to infer object invariants. Our key insight is a new object abstraction for memory objects, where memory is divided into multiple memory banks, each containing several objects. Within each bank, the objects are further abstracted by separating the most recently used (MRU) object, represented precisely with strong updates, while the rest are summarized. For an effective implementation of this approach, we introduce a new composite abstract domain, which forms a reduced product of numerical and equality sub-domains. This design efficiently expresses relationships between a small number of variables (e.g., fields of the same abstract object). We implement the new domain in the CRAB abstract interpreter and evaluate it on several benchmarks for memory safety. We show that our approach is significantly more scalable for relational properties than the existing implementation of CRAB. For evaluating precision, we have integrated our analysis as a pre-processing step to SEABMC bounded model checker, and show that it is effective at both discharging assertions during pre-processing, and significantly improving the run-time of SEABMC.

Figures

Figures reproduced from arXiv: 2411.14735 by the authors.

Figure 2
Figure 2. Abstract memory state on line 17 of [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 3
Figure 3. The syntax of CrabIR. i:=0; loop entry assume(i <= 99); 1 p := alloc(@len, 12); 2 sz := i + 1; 3 (@len, plen) := gep(@len, p); 4 store(@len, plen, i); 5 (@cap, pcap) := gep(@len, p + 4); 6 store(@cap, pcap, sz); 7 buf := alloc(@char, sz); 8 (@buf, pbuf) := gep(@len, p + 8); 9 store(@buf, pbuf, buf); 10 ... 11 i := i + 1; assume(i > 99); (a) line 4 sz 7→ 2, i 7→ 1, p 7→ 200016, . . . scalar mb cache storage flag used… view at source ↗
Figure 4
Figure 4. (a) A program, and (b) an execution of line 4 under RUMM. [PITH_FULL_IMAGE:figures/full_fig_p005_4.png] view at source ↗
Figures from the paper (15 more)
Figure 5
Figure 5. Figure 5: CrabIR statements operating under RUMM. as strong updates after abstraction. For this reason, RUMM incorporates caches to improve precision. We argue that RUMM is compatible with CMM – there is a bisimulation between RUMM and CMM semantics. This follows from: (1) RUMM …
Figure 6
Figure 6. Figure 6: Cache operations. σ ∈ State is a tuple: ⟨scalar , mem⟩. We assume findmb maps a field variable and memory state to a memory bank, indicating in which bank the field is stored. Figs. 5 and 6 describe the changes to a program state at each memory and pointer arithmetic s…
Figure 7
Figure 7. Figure 7: (a) Concrete domain and (b) MRUD hierarchy. [PITH_FULL_IMAGE:figures/full_fig_p009_7.png]
Figure 8
Figure 8. Figure 8: Abstract semantic domains. line 7 sz = 2 ∧ i = 1 ∧ . . . used dirty ispack true true true . . . cap = 2 len = 1 ∧ . . . cap = 1 ∧ len = 0 ∧ . . . i ≈ len ∧ sz ≈ cap p base ≈ cachebase ∧ . . . scalar mb esf ep cache cache sum flag after reduce [PITH_FULL_IMAGE:figures/…
Figure 10
Figure 10. Figure 10: Abstract transformers for memory operations. [PITH_FULL_IMAGE:figures/full_fig_p010_10.png]
Figure 11
Figure 11. Figure 11: Abstract cache operations. operation merges cache into sum. The invariants of the first cached object are copied to sum because, initially, sum does not represent any concrete objects. We change the flag ispk to true since the sum now holds the invariants for that obj…
Figure 12
Figure 12. Figure 12: Fixpoint computation for the entry state of the loop in Fig. 4a. [PITH_FULL_IMAGE:figures/full_fig_p012_12.png]
Figure 13
Figure 13. Figure 13: Domain reduction. In summary, we introduce MRUD, a composite abstract domain and its cor￾responding transformer for inferring object invariants. As a reduced product of domains for scalars and objects, MRUD is effective for scalable analysis. The re￾duction algorithm …
Figure 14
Figure 14. Figure 14: Scalability results. Summarization refers to [PITH_FULL_IMAGE:figures/full_fig_p014_14.png]
Figure 15
Figure 15. Figure 15: Another C program. Program #A DO DS DR safe safe warn safe warn bytebuf 3 3 0 3 0 3 bytebuf memcpy 3 3 0 3 0 3 bytebuf path 3 3 1 2 1 2 ipc handler 3 3 2 1 2 1 mult bytebuf 3 3 0 3 0 3 object 1 1 0 1 0 1 range 2 2 1 1 0 2 [PITH_FULL_IMAGE:figures/full_fig_p016_15.png]
Figure 16
Figure 16. Figure 16: The AI4BMC pipeline. Category Metric % Metric Number of Cases AI4BMC (Z3) AI4BMC (Y2) Performance Comparison Faster (Time Difference > 5s) > 95% 10 2 others 6 1 Slower (Time Difference > 5s) ≤ 50% 4 2 others 0 4 AbsInt Performance AbsInt Time in AI4BMC time > 40% 65 7…
Figure 17
Figure 17. Figure 17: AI4BMC vs. BMC. speed-up. AbsInt takes under one second on average in all 16 cases. There are 4 cases in which AI4BMC is at least 5s slower than BMC. In two of these, the slowdowns are due to Z3 taking 6s extra solving time on average, which is not surprising since th…
Figure 18
Figure 18. Figure 18: Generic algorithm for the lattice operations. [PITH_FULL_IMAGE:figures/full_fig_p024_18.png]
Figure 20
Figure 20. Figure 20: The join and meet operations. procedure addEqual(m, x, y) r := m ▷ r is copied from m r.make(y) r.union(x, y) return r procedure equals(m, x, y) return m.find(x) = m.find(y) [PITH_FULL_IMAGE:figures/full_fig_p026_20.png]
Figure 21
Figure 21. Figure 21: The addEqual and equals operations [PITH_FULL_IMAGE:figures/full_fig_p026_21.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 20 canonical work pages

  1. [1]

    In: Yi, K

    Balakrishnan, G., Reps, T.W.: Recency-abstraction for heap-allocated storage. In: Yi, K. (ed.) Static Analysis, 13th International Symposium, SAS 2006, Seoul, Korea, August 29-31, 2006, Proceedings. Lecture Notes in Computer Science, vol. 4134, pp. 221–239. Springer (2006). https://doi.org/10.1007/11823230_15, https://doi.org/10.1007/11823230_15 Automatic...

    work page doi:10.1007/11823230_15 2006

  2. [3]

    In: Cytron, R., Gupta, R

    Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min´ e, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Cytron, R., Gupta, R. (eds.) Proceedings of the ACM SIGPLAN 2003 Conference on Program- ming Language Design and Implementation 2003, San Diego, California, USA, June 9-11, 2003. pp. 196–207. ACM (2...

    work page arXiv 2003

  3. [4]

    In: Cortesi, A., Logozzo, F

    Chang, B.E., Leino, K.R.M.: Inferring object invariants: Extended abstract. In: Cortesi, A., Logozzo, F. (eds.) Proceedings of the First International Workshop on Abstract Interpretation of Object-oriented Languages, AIOOL@VMCAI 2005, Paris, France, January 21, 2005. Electronic Notes in Theoretical Computer Science, vol. 131, pp. 63–74. Elsevier (2005). h...

    work page doi:10.1016/j.entcs.2005.0 2005

  4. [5]

    In: Fischer, B.N

    Chase, D.R., Wegman, M.N., Zadeck, F.K.: Analysis of pointers and structures. In: Fischer, B.N. (ed.) Proceedings of the ACM SIGPLAN’90 Conference on Pro- gramming Language Design and Implementation (PLDI), White Plains, New York, USA, June 20-22, 1990. pp. 296–310. ACM (1990). https://doi.org/10.1145/93 542.93585, https://doi.org/10.1145/93542.93585

    work page arXiv 1990

  5. [6]

    In: Aho, A.V., Zilles, S.N., Rosen, B.K

    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979. pp. 269–282. ACM Press (1979). https://doi.org/10.1145/5677 52.567778, https://doi.org/10.1145/567752.567778

    work page arXiv 1979

  6. [7]

    In: Okada, M., Satoh, I

    Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min´ e, A., Monniaux, D., Rival, X.: Combination of abstractions in the astr´ ee static analyzer. In: Okada, M., Satoh, I. (eds.) Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 11th Asian Computing Science Conference, Tokyo, Japan, December 6-8, 2006, Revised Selected Papers...

    doi:10.1007/978-3-540-77505-8_23 2006

  7. [8]

    In: Hofmann, M

    Cousot, P., Cousot, R., Mauborgne, L.: The reduced product of abstract domains and the combination of decision procedures. In: Hofmann, M. (ed.) Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr¨ u...

    work page 2011

  8. [9]

    In: Biere, A., Bloem, R

    Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CA V 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8559, pp. 737–744. Springer (2014).https://doi.org/10.1 007/978-3-319-08867-9_49 , htt...

    doi:10.1007/978-3-319-08867-9_49 2014

Show all 29 references
  1. [10]

    In: Rival, X

    Gange, G., Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J.: Exploit- ing sparsity in difference-bound matrices. In: Rival, X. (ed.) Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 22 Y. Su et al. 2016, Proceedings. Lecture Not...

    2016 doi

  2. [11]

    GNU Project: Gnu core utilities official page, https://www.gnu.org/software/c oreutils/

  3. [12]

    In: Jensen, K., Podelski, A

    Gopan, D., DiMaio, F., Dor, N., Reps, T.W., Sagiv, S.: Numeric domains with summarized dimensions. In: Jensen, K., Podelski, A. (eds.) Tools and Algo- rithms for the Construction and Analysis of Systems, 10th International Con- ference, TACAS 2004, Held as Part of the Joint Eu...

    2004

  4. [13]

    In: Lodaya, K., Mahajan, M

    Gulwani, S., Tiwari, A., Necula, G.C.: Join algorithms for the theory of unin- terpreted functions. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004: Founda- tions of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16...

    2004 doi

  5. [14]

    In: Bloem, R., Dimitrova, R., Fan, C., Sharygina, N

    Gurfinkel, A., Navas, J.A.: Abstract interpretation of LL VM with a region-based memory model. In: Bloem, R., Dimitrova, R., Fan, C., Sharygina, N. (eds.) Software Verification - 13th International Conference, VSTTE 2021, New Haven, CT, USA, October 18-19, 2021, and 14th Inter...

    2021 doi

  6. [15]

    In: American Fed- eration of Information Processing Societies: 1982 National Computer Conference, 7-10 June, 1982, Houston, Texas, USA

    Huston, B.: Single-chip microcomputers can be easy to program. In: American Fed- eration of Information Processing Societies: 1982 National Computer Conference, 7-10 June, 1982, Houston, Texas, USA. AFIPS Conference Proceedings, vol. 51, pp. 85–93. AFIPS Press (1982). https://...

    1982

  7. [16]

    In: Podelski, A

    Journault, M., Min´ e, A., Ouadjaout, A.: Modular static analysis of string ma- nipulations in C programs. In: Podelski, A. (ed.) Static Analysis - 25th Interna- tional Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceed- ings. Lecture Notes in Computer Science...

    2018 doi

  8. [17]

    In: Eiter, T., Sands, D

    Kahsai, T., Kersten, R., R¨ ummer, P., Sch¨ af, M.: Quantified heap invariants for object-oriented programs. In: Eiter, T., Sands, D. (eds.) LPAR-21, 21st Inter- national Conference on Logic for Programming, Artificial Intelligence and Rea- soning, Maun, Botswana, May 7-12, 20...

    2017 doi

  9. [18]

    Acta Informatica 6, 133–151 (1976)

    Karr, M.: Affine relationships among variables of a program. Acta Informatica 6, 133–151 (1976). https://doi.org/10.1007/BF00268497 , https://doi.org/10.1 007/BF00268497

    1976 doi

  10. [19]

    In: Sarkar, V., Hall, M.W

    Lattner, C., Adve, V.S.: Automatic pool allocation: improving performance by controlling data structure layout in the heap. In: Sarkar, V., Hall, M.W. (eds.) Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, Jun...

    2005

  11. [20]

    Prentice-Hall, Inc., USA (1997)

    Meyer, B.: Object-oriented software construction (2nd ed.). Prentice-Hall, Inc., USA (1997)

    1997

  12. [21]

    In: Danvy, O., Filinski, A

    Min´ e, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) Programs as Data Objects, Second Symposium, PADO 2001, Aarhus, Denmark, May 21-23, 2001, Proceedings. Lecture Notes in Computer Science, vol. 2053, pp. 155–172. S...

    2001 doi

  13. [22]

    In: Burd, E., Aiken, P., Koschke, R

    Min´ e, A.: The octagon abstract domain. In: Burd, E., Aiken, P., Koschke, R. (eds.) Proceedings of the Eighth Working Conference on Reverse Engineering, WCRE’01, Stuttgart, Germany, October 2-5, 2001. p. 310. IEEE Computer Society (2001). https://doi.org/10.1109/WCRE.2001.957...

    2001

  14. [23]

    In: Sankara- narayanan, S., Sharygina, N

    Monat, R., Ouadjaout, A., Min´ e, A.: Mopsa-c: Modular domains and relational abstract interpretation for C programs (competition contribution). In: Sankara- narayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th Internatio...

    2023

  15. [24]

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

    de Moura, L.M., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint Eu- ropean Conferences on Theory and Pra...

    2008 doi

  16. [25]

    In: Notes of the ACM SIGPLAN Workshop on ML

    Okasaki, C., Gill, A.: Fast mergeable integer maps. In: Notes of the ACM SIGPLAN Workshop on ML. pp. 77–86 (1998)

    1998

  17. [26]

    In: Griggio, A., Rungta, N

    Priya, S., Su, Y., Bao, Y., Zhou, X., Vizel, Y., Gurfinkel, A.: Bounded model checking for LL VM. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022. pp. 214–224. IEEE (2022). https://doi.org/10.34727...

    2022 doi

  18. [27]

    In: Hermenegildo, M.V., Palsberg, J

    Rondon, P.M., Kawaguchi, M., Jhala, R.: Low-level liquid types. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Sym- posium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. pp. 131–144. ACM (2010). ht...

    2010

  19. [28]

    In: M¨ uller-Olm, M., Seidl, H

    Toubhans, A., Chang, B.E., Rival, X.: An abstract domain combinator for sepa- rately conjoining memory abstractions. In: M¨ uller-Olm, M., Seidl, H. (eds.) Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, Septem- ber 11-13, 2014. Proceedings. Lecture ...

    2014 doi

  20. [30]

    18: Generic algorithm for the lattice operations

    ≡ let ⟨scalar1, esf 1, ep 1, mem 1⟩ = σ♯ 1 in let ⟨scalar2, esf 2, ep 2, mem 2⟩ = σ♯ 2 in for allmb1 ∈ mem 1 do mb1 := flushCache♯(mb1) ▷ Update mb1 directly for allmb2 ∈ mem 2 do mb2 := flushCache♯(mb2) ▷ Update mb2 directly ⟨scalar1 op♯ scalar2, esf 1 op♯ esf 2, ep 1 op♯ ep ...

  21. [529]

    https://doi.org/10.1007/978- 3- 540- 24730- 2_38 , https://doi.org/10.1007/978-3-540-24730-2_38

    Springer (2004). https://doi.org/10.1007/978- 3- 540- 24730- 2_38 , https://doi.org/10.1007/978-3-540-24730-2_38

    2004 doi

Pith tools

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