newsSeparation Logic in Coq - News: Topsy Heap Manager verification 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

08/02/06: Topsy Heap Manager verification completed

Item posted by nicolas marti <alalme> on Wed 08 Feb 2006 06:34:58 AM UTC.

The verification of the library used by the Topsy operating system for memory allocation is completed. It includes:
1) the hmInit function: the version in topsy_hmInit.v is manual,
the version in topsy_hmInit_frag.v is semi-automatic (it relies in the decision procedure in frag.v)
2) the hmAlloc function: the version in topsy_hmAlloc.v is the same as in [Marti et al., SPACE 2006]), we are currently working on more precise specifications
3) the hmFree function (in topsy_hmFree.v)



 

Back to the top

Powered by Savane 3.13-4448.
Corresponding source code