> what if I want to reason about larger programs that dynamically allocate, where the addresses may not be known statically? How can I make sure these do not overlap?

We are actively working on this, as it is a pre-condition :P to reason about the simplest of useful programs. The idea is to develop an API around separation logic that allows you to reason about logic that manipulate non-overlapping regions of memory.

It won't be relevant if address are not known statically since API theorems will be parametrized over non-relevant constants such as addresses, function indices, etc...

> And since this is a shallow embedding into lean, what’s the approach for verifying properties of non-terminating programs?

To use the interpreter there is the concept of fuel, which we explicitly hide from the reasoning layer. Using fuel you can write statements of the form, this function returns out of fuel for any value of fuel passed to the interpreter, which is equivalent to prove that your program doesn't terminate.