newsSeparation Logic in Coq - News

 
 

27/01/06:Decision procedure complete

Item posted by nicolas marti <alalme> on Thu 26 Jan 2006 08:52:17 AM UTC.

The decision procedure for a fragment of separation logic (located in frag.v) is now complete and axiom free. The file also contains two examples:

  *) a swap of two cells values
  *) a verification of the initialization function of the Topsy  operating system heap manager




Back to the top

Powered by Savane 3.13-caa5.
Corresponding source code