The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Thanks for making this stuff available.  We're also working on 
separation logic tactics as a central part of the Ynot project, which 
provides support for writing and verifying imperative programs in Coq.  
Reading your paper, I realized that we hadn't included a version of your 
linked-list-reversal example in our distribution, and that needed to be 
rectified. :)

We just released a new Ynot tarball that has such an example, available at:
   http://ynot.cs.harvard.edu/
The reversal example is in examples/Data/Reverse.v in the distribution.

Our approach is much more centered on automation.  My implementation of 
the reversal example contains one lemma about functional lists that 
could just as well be in the Coq List library.  Besides that, about 30 
words of Ltac are required to verify the function, compared to about 200 
in your version.  The Ynot proofs are completely automated; those 30 
words just go towards explaining some proof hints to our parameterized 
separation solver.

The task is easier for us, working in a high-level language, but that's 
mostly orthogonal to the separation proof issues.  Our general-purpose 
separation solver doesn't know anything about lists or the specifics of 
this example.

Andrew McCreight wrote:
> I've just put up a draft paper and accompanying Coq 8.2 implementation 
> for a comprehensive set of tactics for separation logic for a 
> simplified variant of Cminor.  The goal is to make verifying programs 
> with separation logic as easy as proving things involving Coq's 
> standard logic.  There are two sets of tactics, one for proofs 
> involving separation logic assertions and one for proving verification 
> conditions using a separation logic description of the state.  The 
> separation logic assertion tactics include simplification, 
> rearranging, splitting, matching and rewriting.
>
> It should be fairly portable to other memory implementations.  The 
> tactics are implemented entirely in the Ltac tactic language, some 
> reflectively, some directly.  I've also implemented a tactic womega 
> (not described in the paper) that seems to do a reasonable job at 
> solving goals involving basic 32-bit address arithmetic that I've come 
> across while doing verification.  The implementation also includes a 
> few small examples.
>
> The draft and implementation are available at 
> http://web.cecs.pdx.edu/~mccreigh/ptsl/ 
> <http://web.cecs.pdx.edu/%7Emccreigh/ptsl/>