Translating Separation Logic into
	    Dynamic Frames Using Fine-Grained Region Logic
				  by
	     Yuyan Bao, Gary T. Leavens, and Gidon Ernst
			     
			       Abstract

Several techniques have been proposed for specification and
verification of frame conditions,
making it difficult for specification language designers to know which
to pick.
Ideally there would be a single mechanism that could be used to
express specifications written in all techniques.
In this paper we provide a single mechanism that can be used to write
specifications in the style of both separation logic and dynamic frames.
This mechanism shows common characters between the two methodologies. 

Keywords: Region logic, sequential programming, separation logic, 
dynamic frames, formal methods, frame axioms, DafnyR language.

2013 CR Categories:
D.2.4 [Software Engineering]
    Software/Program Verification -- Formal methods, programming by contract;
F.3.1 [Logics and Meanings of Programs]
    Specifying and Verifying and Reasoning about Programs --
        Assertions, logics of programs, pre- and post-conditions, 
        specification techniques;