newsSeparation Logic in Coq - News: Decision procedure complete

 
 
Latest News
Upadte of Bigtoe posted by alalme, Wed 13 Dec 2006 01:48:39 AM UTC
Update to Coq v8.1 posted by alalme, Wed 13 Dec 2006 01:45:43 AM UTC
extraction of a certified verifier posted by alalme, Thu 21 Sep 2006 01:11:03 AM UTC
Completeness proof for Separation Logic posted by alalme, Thu 10 Aug 2006 08:58:53 AM UTC

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-758e.
Corresponding source code