Any mathematical tools for analyzing mutable memory Wondering if there are any documents, theories, or methodologies for dealing with mutable memory mathematically. Basically a formal algebraic model of how computers manipulate memory. Along the lines of, say I want to model an add operation at a low level, and it writes its output to a register. Then we can model the computer state as a memory, and:

$$add : a \times b \times m \to m'$$

the function $add$ transforms the memory into a different state, holding the final value. Then the second time we call add, the memory is different than it was before. So it's always changing:

$$m \neq m' \neq m'' \neq \dots \neq m^{(n)}$$

Wondering if there are any formalisms out there that deal with this. I would specifically like to see it applied to abstract algebra or category theory. Whereas in abstract algebra typically, everything is immutable and you never worry about "state". I would like to explore the state / mutable memory from a math framework.
See separation logic and theory of arrays in SMT solvers.  Both of these provide a principled, mathematically rigorous foundation for reasoning about mutable memory.