== Separation logic & proof assistants ==

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://flint.cs.yale.edu/flint/software.html|CAP/SCAP/XCAP]] (Yale)
 * [[http://www.cs.princeton.edu/~appel/cminor/|Concurrent C Minor]] (Princeton)
 * [[http://holfoot.heap-of-problems.org/|Holfoot]] (Cambridge)
 * [[http://ertos.nicta.com.au/research/l4.verified/|L4.verified]] (Sydney)
 * [[http://staff.aist.go.jp/reynald.affeldt/seplog/|SepLog in Coq]]  (Tokyo)
 * [[http://ynot.cs.harvard.edu/|Ynot]] (Harvard)

=== Medium-scale and large-scale case studies ===

 * [[http://ynot.cs.harvard.edu/papers/popl10.pdf|Lightweight RDBMS]] (Ynot)
 * [[http://software.imdea.org/~aleks/papers/reflect/reflect.pdf|Fast congrunce closure algorithm of Nieuwenhuis and Oliveras]] (HTT/Ynot)
 * [[http://ertos.nicta.com.au/research/l4.verified/|L4 microkernel]]