mainSeparation Logic in Coq - Summary

Membership Info
Group Admin:
2 active members

Group identification
Id: 8196
System Name: seplog
Name: Separation Logic in Coq
Group Type: non-GNU software and documentation

Search in this Group


This group is not part of the GNU Project.

Our goal is to build a library in Coq based on separation logic to enable verification of memory properties of low-level software. This online CVS provides the current implementation of our library together with examples, including a substantial use-case.

Registration Date: Thu 15 Dec 2005 01:56:40 AM UTC
License: GNU General Public License v2 or later
Development Status: 0 - Undefined


Latest News rss feed
Upadte of Bigtoe
     posted by alalme, 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).

Update to Coq v8.1
     posted by alalme, Wed 13 Dec 2006 01:45:43 AM UTC

We updated every source file of seplog to be compatible with Coq v8.1.

extraction of a certified verifier
     posted by alalme, Thu 21 Sep 2006 01:11:03 AM UTC

We implemented a decision procedure by reflection for Hoare triples using a fragment of separation logic (frag_hoare in frag.v).

Using the abstraction facility of Coq, we extracted the decision procedure in Ocaml, built a parser for Hoare triples with Ocaml-yacc, finally giving a certified verifier for Hoare triples. Its name is bigtoe (any similarity with an existing tool is not a coincidence).

Completeness proof for Separation Logic
     posted by alalme, Thu 10 Aug 2006 08:58:53 AM UTC

Completeness proof for separation logic (lemma semax_complete in axiomatic.v).

Quick Overview
 Memberlist (2 members)

Communication Tools
 Mailing Lists (0 public mailing lists)

Development Tools
 Task Manager (open items: 0, total: 0)
 Patch Manager (open items: 0, total: 0)

Back to the top

Powered by Savane 3.13-b921.
Corresponding source code