Separation Logic in Coq - News

Group

Main
- Main
- View members
- Search
Homepage
Download
Support
- Submit new
- Browse
- Reset to open
- Digest
- Dependencies
- ~~Export~~
- Get statistics
- Search
Mailing lists
Source code
Bugs
- Submit new
- Browse
- Reset to open
- Digest
- Dependencies
- ~~Export~~
- Get statistics
- Search
Tasks
- ~~Submit new~~
- Browse
- Reset to open
- Digest
- Dependencies
- ~~Export~~
- Get statistics
- Search
Patches
- ~~Submit new~~
- Browse
- Reset to open
- Digest
- Dependencies
- ~~Export~~
- Get statistics
- Search
News
- Browse
- Atom feed
- ~~Submit~~
- ~~Manage~~

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)