Resource reasoning in program analysis

The fundamental ideas of the resource logics (linear logic, separation logic) are presented in a semi-formal style. For general resource models, on one hand, and for concrete heap-like models of practical interest, on the other hand, we get into the formalities, including the semantics of the assertion language and axioms and inference rules. Surprisingly, as for the assertion language of separation logic, even purely propositional separation logic turns out to be undecidable, even for a concrete heap-like models of practical interest.