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.

Medium-scale and large-scale case studies

SLInProofAssistants (last edited 2011-02-07 14:25:35 by viktor)