Pith. sign in

REVIEW 5 minor 44 references

Physical separation makes Rowhammer disappear from the protected view of every finite program run, for every admissible fault model.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

Under physical separation, every finite Rowhammer execution projects to the Dirac distribution of the ordinary deterministic run on protected memory, control and access traces, fully mechanised in Lean.

T0 review reviewed 2026-07-14 challenge →

load-bearing objection Clean, fully mechanised PL semantics for Rowhammer with a distribution-independent collapse theorem for physical separation; the modelling restrictions are stated honestly and do not break the proved claims.

arxiv 2607.10314 v1 pith:JFFEJYAA submitted 2026-07-11 cs.PL

Mechanised operational semantics of Rowhammer

Martin Berger , Amir Naseredini This is my paper
classification cs.PL
keywords Rowhammeroperational semanticsprobabilistic fault modelsphysical separationnon-interferenceinformation flowmechanised verificationLean
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

The reading

Conventional programming-language semantics assume that reading or writing one memory location leaves every other location alone. Rowhammer breaks that assumption: hammering one DRAM row can flip bits in nearby rows that the program never touched. This paper supplies a compositional operational semantics that treats those faults as a small probabilistic effect on the ordinary read and write operations of an idealised imperative language, without modelling DRAM physics. The key result is a distribution-independent collapse theorem: if every location a well-formed program uses is placed outside every other such location's blast radius, then the residual program, the protected memory contents, and the access trace after any finite number of steps are exactly those of the ordinary fault-free run, as a Dirac distribution. The same collapse transfers ordinary non-interference into a probability-sensitive Rowhammer setting and reflects every Rowhammer leak back to a leak already present without faults. The whole development is mechanised in Lean.

Core claim

Under an abstract frame-local fault kernel, a safe physical layout, and program well-formedness, the protected projection of every finite probabilistic Rowhammer execution is identical to the corresponding deterministic execution: residual program, memory restricted to protected locations, and access trace coincide as a point mass, independently of the concrete flip probabilities.

What carries the argument

The semantic-collapse theorem (Theorem 6.1 / physical_separation_sound): a probabilistic simulation whose invariant is parametric in a kept region of memory, instantiated by physical separation so that every supported fault outcome leaves protected locations and control flow untouched.

Load-bearing premise

Faults are history-free and stationary: the chance of a flip depends only on the current victim set and the current memory, never on activation history, refresh state, or time.

What would settle it

Exhibit a well-formed program on a safe layout together with a frame-local kernel for which some finite step count yields a protected residual program, protected memory value, or access trace different from the deterministic run; or show that real DRAM faults that depend on charge accumulation produce such a divergence under an otherwise faithful instantiation of the model.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

0 major / 5 minor

Summary. The paper gives a probabilistic small-step operational semantics for a WHILE language under Rowhammer-style faults. Faults are isolated at the read/write interface via an abstract, history-free, frame-local probability kernel; the rest of the semantics is lifted monadically. The main result (Theorem 6.1) is a distribution-independent collapse: under physical separation and program well-formedness, the protected projection of every finite n-step Rowhammer run is exactly the Dirac distribution of the ordinary deterministic run (residual program, protected memory, access trace). Observation-parametric non-interference is then shown to be preserved and reflected by the same collapse. The entire development is mechanised in Lean 4/mathlib with an explicit axiom audit (only propext, Classical.choice, Quot.sound).

Significance. This is a genuine bridge between DRAM disturbance research and programming-language security. The collapse theorem is distribution-free, covers terminating and non-terminating prefixes, and is fully machine-checked; the non-interference results are direct corollaries rather than a second simulation. The small fault-kernel interface is language-parametric in principle and recovers ordinary semantics by the no-fault embedding (Theorem 6.4). For a venue that values mechanised semantics and hyperproperties, the contribution is substantial and the artefact is a clear strength.

minor comments (5)
  1. [§5.1] Section 5.1, clauses (F3)–(F4): history-freeness and stationarity are correctly flagged as modelling restrictions that exclude charge accumulation and refresh effects. A short forward pointer in the introduction or abstract to the future-work discussion in Section 10 would help readers who expect a device-level model.
  2. [§5.6] Section 5.6: mixed termination is illustrated but limiting probabilities of divergence are not mechanised. The finite-step approach is sufficient for the proved theorems; a one-sentence clarification that the paper makes no claim about eventual termination probabilities would avoid over-reading.
  3. [§8.1] Section 8.1: the four concrete observers are useful, but the text already notes that the fourth is not classical termination-insensitive NI. Making that caveat slightly more prominent (e.g., in the definition list) would prevent mis-citation.
  4. [§5.3] Figures 2–4 and the distance-based SeparationModel instance are clear; a brief remark that numerical address distance is only a witness, not a claim about physical DRAM geometry, already appears but could be repeated near the first use of the concrete instance.
  5. A few typographical nits (e.g., spacing around ‘i.e.’, occasional long lines in Lean excerpts) do not affect readability but could be cleaned in production.

Circularity Check

0 steps flagged

No significant circularity: collapse and non-interference theorems are non-trivial consequences of an explicit abstract fault contract, proved by parametric simulation and fully mechanised.

full rationale

The paper defines a probabilistic small-step semantics by reinterpreting the ordinary read/write interface as Dist-valued kernels (Section 5), subject to an explicit four-clause fault-kernel contract (F1–F4). Theorem 6.1 (PhysicalSeparationSound) then states that, under frame-locality, safe separation and well-formedness, the protected-view projection of every finite Rowhammer run equals the Dirac mass of the corresponding deterministic run. The proof is a standard one-step invariant (stepRHHat_agree) iterated by induction on step count (runRHTrace_protected), instantiated at keep = membership in the protected set; the same collapse immediately yields the observation-parametric non-interference equivalence (Theorems 8.4–8.6). None of these steps reduces by construction to its inputs: the Dirac equality is false without the three hypotheses, the no-fault embedding (Theorem 6.4) recovers ordinary semantics only for the identity kernel, and the development contains no fitted parameters, no load-bearing self-citation of an unverified uniqueness claim, and no smuggled ansatz. The history-freeness/stationarity restrictions (F3–F4) are openly declared modelling boundaries, not hidden circular premises. The entire argument is self-contained, machine-checked in Lean/mathlib with only the three foundational axioms, and therefore exhibits zero circularity of the kinds enumerated.

Axiom & Free-Parameter Ledger

0 free parameters · 6 axioms · 3 invented entities

The theorems rest on an abstract fault-kernel contract and a separation geometry; there are no free numerical parameters. All probabilistic reasoning uses the standard discrete probability monad. The only non-standard modelling choices are the four clauses of the fault contract, of which history-freeness and stationarity are explicitly flagged as restrictions. Invented entities are pure formal interfaces, not new physical objects.

axioms (6)
  • domain assumption Frame-locality (F2): every memory in the support of a fault agrees with the pre-fault memory outside the victim set
    Sole behavioural hypothesis on the kernel; used in every step of the collapse proof (§5.1, §6.4).
  • domain assumption History-freeness (F3) and stationarity (F4): the kernel is a pure function of current victim set and memory, independent of access history and time
    Encoded by the type of ProbRHFlip; excludes charge accumulation and refresh effects; flagged by the authors as a genuine restriction.
  • domain assumption Access-triggered faults (F1): faults are sampled exactly at read(x) and write(x) transitions; tau-steps are Dirac
    Enforced by construction of the transition rules; localises the probabilistic effect.
  • domain assumption Safe separation implies protected–victim disjointness (safe_disjoint)
    The single geometric fact required by the soundness proof; abstract over concrete DRAM row layouts.
  • standard math Discrete probability monad (Giry/PMF) with Dirac, bind and map
    Standard mathlib infrastructure; no new probability axioms added.
  • standard math Lean foundational axioms (propext, Classical.choice, Quot.sound)
    Confirmed by the paper’s axiom-audit script; no problem-specific axioms.
invented entities (3)
  • Probabilistic fault-kernel interface (ProbRHFlip + HasProbFlipFrame) no independent evidence
    purpose: Abstract Rowhammer as a probability kernel from victim set and memory to successor memories, isolating the effect at the read/write boundary.
    Purely formal modelling device; no independent physical prediction beyond the abstract contract.
  • SeparationModel (adj, isSafe, safe_disjoint) no independent evidence
    purpose: Parameterise blast-radius geometry so the collapse theorem is independent of any particular DRAM organisation.
    Abstract structure; concrete distance instance is only a non-vacuity witness.
  • Protected view (protView) and observation-parametric observers no independent evidence
    purpose: Project residual program, protected memory and access trace so that security properties become direct corollaries of semantic collapse.
    Definitional projection; not a new physical entity.

reviewed 2026-07-14 · how reviews work

0 comments
Cite this review

Pith. "Pith review of Mechanised operational semantics of Rowhammer." pith.science (2026). https://pith.science/paper/JFFEJYAA

@misc{pith2026260710314,
  author       = {Pith},
  title        = {Pith review of: Mechanised operational semantics of Rowhammer},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JFFEJYAA}},
  note         = {Machine review of arXiv:2607.10314}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

Rowhammer is a hardware vulnerability in dynamic random-access memory (DRAM) in which repeated accesses to aggressor rows can induce bit-flips in victim rows. This phenomenon violates a core assumption of conventional programming language semantics: reading or writing one memory location does not modify others. Despite the security importance of this phenomenon, there is no formal framework connecting Rowhammer faults with program behaviour. We present a probabilistic small-step operational semantics for an idealised imperative language subject to Rowhammer-style faults. The semantics abstracts from DRAM internals and semiconductor physics. A general probabilistic fault model parameterises the semantics, representing Rowhammer-style faults by assigning probabilities to bit-flips during read or write operations. The resulting distributions are propagated through programs using the standard monadic structure of probabilistic computation. As a case study, we formalise a well-known defence that places program variables sufficiently far apart in physical memory that an access to one variable cannot disturb another. We prove a distribution-independent semantic collapse theorem: for every finite execution, including prefixes of terminating and non-terminating executions, the protected projection of the probabilistic Rowhammer semantics is the Dirac distribution of the corresponding Rowhammer-free execution. We develop an observation-parametric account of secure information flow. Non-interference is expressed as a hyperproperty comparing the distributions of low observations from low-equivalent initial memories. Consequently, physical separation preserves non-interference for every admissible fault model, while every Rowhammer non-interference violation reflects a violation already present in the Rowhammer-free semantics. The development is fully mechanised in Lean using mathlib.

Figures

Figures reproduced from arXiv: 2607.10314 by Amir Naseredini, Martin Berger.

Figure 1
Figure 1. Figure 1: The memory hierarchy. Each level trades speed for capacity. DRAM (highlighted) wins its place through [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Disturbance is local. Repeatedly activating ( [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Physical separation with a blast radius of [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The idea behind the fault model is that each variable [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

44 extracted references · 12 canonical work pages · 1 internal anchor

  1. [1]

    Mechanised operational semantics of Rowhammer

    Anonymous. 2026. Lean proofs for "Mechanised operational semantics of Rowhammer". https://anonymous.4open. science/r/rh_separation_paper_anon_lean-48C7/

    2026

  2. [2]

    Ferdinand Brasser, Lucas Davi, David Gens, Christopher Liebchen, and Ahmad-Reza Sadeghi. 2017. CAn’t Touch This: Software-only Mitigation against Rowhammer Attacks Targeting Kernel Memory. In26th USENIX Security Symposium (USENIX Security 17). USENIX Association, Vancouver, BC, Canada, 117–130. https://www.usenix.org/conference/ usenixsecurity17/technical...

    2017

  3. [3]

    Clarkson and Fred B

    Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties.Journal of Computer Security18, 6 (2010), 1157–1210. doi:10.3233/JCS-2009-0393

    doi:10.3233/jcs-2009-0393 2010

  4. [4]

    Paul J. Cohen. 1963. The Independence of the Continuum Hypothesis.Proceedings of the National Academy of Sciences 50, 6 (1963), 1143–1148. doi:10.1073/pnas.50.6.1143

    doi:10.1073/pnas.50.6.1143 1963

  5. [6]

    Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. InAutomated Deduction – CADE 28. Springer, 625–635. doi:10.1007/978-3-030-79876-5_37

    doi:10.1007/978-3-030-79876-5_37 2021

  6. [7]

    Pietro Frigo, Emanuele Vannacci, Hasan Hassan, Victor van der Veen, Onur Mutlu, Cristiano Giuffrida, Herbert Bos, and Kaveh Razavi. 2020. TRRespass: Exploiting the Many Sides of Target Row Refresh. In2020 IEEE Symposium on Security and Privacy (SP). 747–762. doi:10.1109/SP40000.2020.00090

    doi:10.1109/sp40000.2020.00090 2020

  7. [8]

    Michèle Giry. 1982. A categorical approach to probability theory. InCategorical Aspects of Topology and Analysis. Lecture Notes in Mathematics, Vol. 915. Springer, 68–85. doi:10.1007/BFb0092872

    doi:10.1007/bfb0092872 1982

  8. [9]

    1940.The Consistency of the Continuum-Hypothesis

    Kurt Gödel. 1940.The Consistency of the Continuum-Hypothesis. Number 3 in Annals of Mathematics Studies. Princeton University Press, Princeton, NJ. doi:10.1515/9781400881635

    work page doi:10.1515/9781400881635 1940

  9. [10]

    Goguen and José Meseguer

    Joseph A. Goguen and José Meseguer. 1982. Security Policies and Security Models. InProceedings of the 1982 IEEE Symposium on Security and Privacy. 11–20. doi:10.1109/SP.1982.10014

    doi:10.1109/sp.1982.10014 1982

  10. [11]

    Daniel Gruss, Clémentine Maurice, and Stefan Mangard. 2016. Rowhammer.js: A Remote Software-Induced Fault Attack in JavaScript. InDetection of Intrusions and Malware, and Vulnerability Assessment (DIMV A). Springer, 300–321. doi:10.1007/978-3-319-40667-1_15

    work page doi:10.1007/978-3-319-40667-1_15 2016

  11. [12]

    Kurt Gödel. 1933. On Intuitionistic Arithmetic and Number Theory.Ergebnisse eines mathematischen Kolloquiums4 (1933), 34–38. doi:10.1093/oso/9780195147209.003.0063 English translation by Stefan Bauer-Mengelberg and Jean van Heijenoort. Reprinted in:Kurt Gödel: Collected Works, Volume I, Oxford University Press (1986)

    doi:10.1093/oso/9780195147209.003.0063 1933

  12. [13]

    Kim, Victor van der Veen, Kaveh Razavi, and Onur Mutlu

    Hasan Hassan, Yahya Can Tuğrul, Jeremie S. Kim, Victor van der Veen, Kaveh Razavi, and Onur Mutlu. 2021. Uncovering In-DRAM RowHammer Protection Mechanisms: A New Methodology, Custom RowHammer Patterns, and Implications. In54th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO-54). doi:10.1145/3466752.3480110

    doi:10.1145/3466752.3480110 2021

  13. [14]

    Sebastian Hunt, David Sands, and Sandro Stucki. 2023. Reconciling Shannon and Scott with a Lattice of Computable Information.Proc. ACM Program. Lang.7, POPL, Article 68 (jan 2023), 30 pages. doi:10.1145/3571740

    work page doi:10.1145/3571740 2023

  14. [15]

    Patrick Jattke, Victor van der Veen, Pietro Frigo, Stijn Gunter, and Kaveh Razavi. 2022. BLACKSMITH: Scalable Rowhammering in the Frequency Domain. In2022 IEEE Symposium on Security and Privacy (SP). 716–734. doi:10.1109/ SP46214.2022.9833772

    arXiv 2022

  15. [16]

    Yoongu Kim, Ross Daly, Jeremie Kim, Chris Fallin, Ji Hye Lee, Donghyuk Lee, Chris Wilkerson, Konrad Lai, and Onur Mutlu. 2014. Flipping Bits in Memory Without Accessing Them: An Experimental Study of DRAM Disturbance Errors. InProceedings of the 41st Annual International Symposium on Computer Architecture (ISCA ’14). 361–372. doi:10.1109/ISCA.2014.6853210

    doi:10.1109/isca.2014.6853210 2014

  16. [17]

    Andreas Kogler, Jonas Juffinger, Sulaiman Qazi, Yoongu Kim, Moritz Lipp, Nicolas Boichat, Eric Shiu, Matt Nissler, and Daniel Gruss. 2022. Half-Double: Hammering From the Next Row Over. In31st USENIX Security Symposium (USENIX Security 22). USENIX Association, 3807–3824. https://www.usenix.org/conference/usenixsecurity22/presentation/ kogler-half-double

    2022

  17. [18]

    Radhesh Krishnan Konoth, Marco Oliverio, Andrei Tatar, Dennis Andriesse, Herbert Bos, Cristiano Giuffrida, and Kaveh Razavi. 2018. ZebRAM: Comprehensive and Compatible Software Protection Against Rowhammer Attacks. In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18). USENIX Association. https: //www.usenix.org/conference/osdi...

    2018

  18. [19]

    Dexter Kozen. 1981. Semantics of Probabilistic Programs.J. Comput. System Sci.22, 3 (1981), 328–350. doi:10.1016/0022- 0000(81)90036-2

    doi:10.1016/0022- 1981

  19. [20]

    Andrew Kwong, Daniel Genkin, Daniel Gruss, and Yuval Yarom. 2020. RAMBleed: Reading Bits in Memory Without Accessing Them. InIEEE Symposium on Security and Privacy (S&P). IEEE, 695–711. doi:10.1109/SP40000.2020.00020

    doi:10.1109/sp40000.2020.00020 2020

  20. [21]

    Francis William Lawvere. 1962. The Category of Probabilistic Mappings: With Applications to Stochastic Processes, Statistics, and Pattern Recognition. (1962). https://lawverearchives.com/wp-content/uploads/2025/07/1962.probmap. pdf Manuscript, 12 pages. Mechanised operational semantics of Rowhammer 27

    1962

  21. [22]

    1998.Categories for the Working Mathematician(2 ed.)

    Saunders Mac Lane. 1998.Categories for the Working Mathematician(2 ed.). Graduate Texts in Mathematics, Vol. 5. Springer, New York. doi:10.1007/978-1-4757-4721-8

    doi:10.1007/978-1-4757-4721-8 1998

  22. [23]

    John McCarthy. 1962. Towards a Mathematical Science of Computation. InInformation Processing 1962: Proceedings of IFIP Congress 62, Cicely M. Popplewell (Ed.). North-Holland, Amsterdam, 21–28. https://www-formal.stanford.edu/ jmc/towards.pdf

    1962

  23. [24]

    Eugenio Moggi. 1991. Notions of Computation and Monads.Information and Computation93, 1 (1991), 55–92. doi:10.1016/0890-5401(91)90052-4

    doi:10.1016/0890-5401(91)90052-4 1991

  24. [25]

    Peter D. Mosses. 2004. Modular Structural Operational Semantics.Journal of Logical and Algebraic Methods in Programming60–61 (2004), 195–228. doi:10.1016/j.jlap.2004.03.008

    work page doi:10.1016/j.jlap.2004.03.008 2004

  25. [26]

    Onur Mutlu and Jeremie S. Kim. 2020. RowHammer: A Retrospective.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems39, 8 (2020), 1555–1571. doi:10.1109/TCAD.2019.2915318

    doi:10.1109/tcad.2019.2915318 2020

  26. [27]

    2024.Towards Automatic Analysis of Microarchitectural Attacks

    Amir Naseredini. 2024.Towards Automatic Analysis of Microarchitectural Attacks. Ph. D. Dissertation. University of Sussex. https://sussex.figshare.com/articles/thesis/Towards_automatic_analysis_of_microarchitectural_attacks/ 24610929

    2024

  27. [28]

    Amir Naseredini, Martin Berger, Matteo Sammartino, and Shale Xiong. 2023. ALARM: Active LeArning of Rowhammer Mitigations. InProceedings of the 11th International Workshop on Hardware and Architectural Support for Security and Privacy(Chicago, IL, USA)(HASP ’22). Association for Computing Machinery, New York, NY, USA, 1–9. doi:10.1145/ 3569562.3569563

    arXiv 2023

  28. [30]

    Giray Yağlıkçı, Haocong Luo, Ataberk Olgun, Jisung Park, Hasan Hassan, Minesh Patel, Jeremie S

    Lois Orosa, A. Giray Yağlıkçı, Haocong Luo, Ataberk Olgun, Jisung Park, Hasan Hassan, Minesh Patel, Jeremie S. Kim, and Onur Mutlu. 2021. A Deeper Look into RowHammer’s Sensitivities: Experimental Analysis of Real DRAM Chips and Implications on Future Attacks and Defenses. In54th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO-54). doi...

    doi:10.1145/3466752.3480069 2021

  29. [31]

    Thibaut Pérami, Thomas Bauereiss, Brian Campbell, Zongyuan Liu, Nils Lauermann, Alasdair Armstrong, and Peter Sewell. 2026. ArchSem: Reusable Rigorous Semantics of Relaxed Architectures.Proc. ACM Program. Lang.10, POPL (2026), 204–234. doi:10.1145/3776650

    work page doi:10.1145/3776650 2026

  30. [32]

    Gordon Plotkin and John Power. 2002. Notions of Computation Determine Monads. InFoundations of Software Science and Computation Structures (Lecture Notes in Computer Science, Vol. 2303). Springer, 373–393. doi:10.1007/3-540-45931- 6_24

    work page doi:10.1007/3-540-45931- 2002

  31. [33]

    Norman Ramsey and Avi Pfeffer. 2002. Stochastic lambda calculus and monads of probability distributions. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 154–165. doi:10.1145/503272.503288

    doi:10.1145/503272.503288 2002

  32. [34]

    Andrei Sabelfeld and Andrew C. Myers. 2003. Language-Based Information-Flow Security.IEEE Journal on Selected Areas in Communications21, 1 (2003), 5–19. doi:10.1109/JSAC.2002.806121

    doi:10.1109/jsac.2002.806121 2003

  33. [35]

    Mark Seaborn and Thomas Dullien. 2015. Exploiting the DRAM rowhammer bug to gain kernel privileges. https: //googleprojectzero.blogspot.com/2015/03/exploiting-dram-rowhammer-bug-to-gain.html Code at https://github. com/google/rowhammer-test

    2015

  34. [36]

    Claude E. Shannon. 1948. A Mathematical Theory of Communication.The Bell System Technical Journal27, 3 (1948), 379–423. doi:10.1002/j.1538-7305.1948.tb01338.x

    doi:10.1002/j.1538-7305.1948.tb01338.x 1948

  35. [37]

    The mathlib Community. 2020. The Lean Mathematical Library. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs(New Orleans, LA, USA)(CPP 2020). Association for Computing Machinery, New York, NY, USA, 367–381. doi:10.1145/3372885.3373824

    doi:10.1145/3372885.3373824 2020

  36. [38]

    Cláudio Vasconcelos and António Ravara. 2016. The While language. arXiv:1603.08949 [cs.PL] doi:10.48550/arXiv. 1603.08949

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv 2016

  37. [39]

    Andrew Walker, Sungkwon Lee, and Dafna Beery. 2021. On DRAM Rowhammer and the Physics of Insecurity.IEEE Transactions on Electron DevicesPP (03 2021), 1–11. doi:10.1109/TED.2021.3060362

    work page doi:10.1109/ted.2021.3060362 2021

  38. [40]

    Giray Yağlıkçı, Minesh Patel, Jeremie S

    A. Giray Yağlıkçı, Minesh Patel, Jeremie S. Kim, Roknoddin Azizi, Ataberk Olgun, Lois Orosa, Hasan Hassan, Jisung Park, Konstantinos Kanellopoulos, Taha Shahroodi, Saugata Ghose, and Onur Mutlu. 2021. BlockHammer: Preventing RowHammer at Low Cost by Blacklisting Rapidly-Accessed DRAM Rows. InIEEE International Symposium on High- Performance Computer Archi...

    doi:10.1109/hpca51647.2021.00037 2021

  39. [41]

    2020.Semantics of Probabilistic Programming: A Gentle Introduction

    Fredrik Dahlqvist, Alexandra Silva, and Dexter Kozen. 2020.Semantics of Probabilistic Programming: A Gentle Introduction. Cambridge University Press, 1–42. doi:10.1017/9781108770750.002

    work page doi:10.1017/9781108770750.002 2020

  40. [42]

    Alessandra Di Pierro, Chris Hankin, and Herbert Wiklicky. 2010. Probabilistic Semantics and Program Analysis. In Lecture Notes in Computer Science. Springer Berlin Heidelberg, 1–42. doi:10.1007/978-3-642-13678-8_1

    work page doi:10.1007/978-3-642-13678-8_1 2010

  41. [43]

    Ugo Dal Lago and Margherita Zorzi. 2012. Probabilistic operational semantics for the lambda calculus.RAIRO - Theoretical Informatics and Applications46 (2012), 413–450. doi:10.1051/ita/2012012

    doi:10.1051/ita/2012012 2012

  42. [44]

    2007.Semantics with Applications: An Appetizer (Undergraduate Topics in Computer Science)

    Hanne Riis Nielson and Flemming Nielson. 2007.Semantics with Applications: An Appetizer (Undergraduate Topics in Computer Science). Springer-Verlag, Berlin, Heidelberg. doi:10.1007/978-1-84628-692-6

    doi:10.1007/978-1-84628-692-6 2007

  43. [45]

    2014.Concrete Semantics: With Isabelle/HOL

    Tobias Nipkow and Gerwin Klein. 2014.Concrete Semantics: With Isabelle/HOL. Springer. doi:10.1007/978-3-319-10542-0 Mechanised operational semantics of Rowhammer 35

    work page doi:10.1007/978-3-319-10542-0 2014

  44. [46]

    1993.The Formal Semantics of Programming Languages

    Glynn Winskel. 1993.The Formal Semantics of Programming Languages. The MIT Press. doi:10.7551/mitpress/3054.001. 0001

    work page doi:10.7551/mitpress/3054.001 1993

This paper was first reviewed by grok-4.5 on July 14, 2026.