Principles for Verification Tools: Separation Logic

Brijesh Dongol, Victor B. F. Gomes, Georg Struth

A principled approach to the design of program verification and con- struction tools is applied to separation logic. The control flow is modelled by power series with convolution a…