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~~

Verification of a new specification for the memory allocator of Topsy

Item posted by nicolas marti <alalme> on Mon 07 Aug 2006 12:29:04 AM UTC.

We have completed the verification of a new specification for the dynamic memory allocator of the Topsy operating system. The previous specification had the following inconvenient: an allocator that always fails was correct. The new specification is more
precise, it asserts that if there is enough free memory (modulo compaction), then the allocation always succeeds. The specification and its proof are in the file topsy_hmAlloc2.v.