Separation Logic in Coq - News: Upadte of Bigtoe
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 posted by alalme, Mon 07 Aug 2006 12:29:04 AM UTC
Upadte of Bigtoe
Item posted by nicolas marti <alalme> on Wed 13 Dec 2006 01:48:39 AM UTC.
We updated the decision procedure for separation logic with loops.
The Coq source code is frag2.v. The directory bigtoe2 contains an Ocaml verifier extracted from frag2.v. This verifier comes with several examples (sub-directory examples).
Powered by Savane 3.13-f8d8.
Corresponding source code