The Coq mailing list

[Andrew McCreight <continuation AT gmail.com>]

Hello all,

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/


Andrew McCreight
HASP Project
Portland State University

http://hasp.cs.pdx.edu/