== Program Analysis based on Separation Logic ==

As is incredibly difficult for fully automatic techniques to prove full functional correctness, a number of projects use separation logic within a proof assistant (in the sense of the LCF/HOL/Isabelle/Coq tradition). Often these interactive proofs are assisted by advanced tactics that carry out many mundane proof steps.

 * [[http://research.microsoft.com/en-us/um/cambridge/projects/slayer/|SLAyer]] (Microsoft Cambridge)
 

=== Case Studies ===

 * [[whatever.html|to add]] (wherever)