(web page under construction!)
There are a number of lines of research on separation logic. One is to work towards the automated verification of software to ensure safety and dependability. It aims to address one of the grand challenge issues in computer science, to make verified software a reality. Two tools have been developed: SLEEK is an entailment prover for separation logic formula, while HIP is a verifier for an imperative language that supports specification of data structures with strong invariant properties.
Another line of research is on semantic modeling focused on models for separation logic, particularly separation logic with higher-order features. This included work on separation algebras and share accounting, as well as methods to approximate an important class of recursive domain equations.
Also released is a library for the mechanized theorem prover Coq focusing on supporting semantic models for programming language research, http://msl.cs.princeton.edu. This library has begun to get some traction and independent citations.