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 - 0 replies
Update to Coq v8.1 posted by alalme, Wed 13 Dec 2006 01:45:43 AM UTC - 0 replies
extraction of a certified verifier posted by alalme, Thu 21 Sep 2006 01:11:03 AM UTC - 0 replies
Completeness proof for Separation Logic posted by alalme, Thu 10 Aug 2006 08:58:53 AM UTC - 0 replies

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

No messages in 27/01/06:Decision procedure complete


Back to the top

Powered by Savane 3.9