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

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