newsSeparation 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

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).

 

Back to the top

Powered by Savane 3.13-f8d8.
Corresponding source code