newsSeparation Logic in Coq - News

 
 

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-d3ae.
Corresponding source code