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.

• Any undergrad textbook on semantics should get you started. (Eike Best's 1996 Book comes to mind.) How complicated all that becomes depends on what language features you want to model. Category (or domain) theory enters the picture when higher order functions are to be modelled. – Kai May 24 '18 at 8:35