newsSeparation Logic in Coq - News: Verification of another specification for the memory allocator of Topsy

 
 
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

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.


 

Back to the top

Powered by Savane 3.13-d3ae.
Corresponding source code