newsSeparation Logic in Coq - News

Show summaries for the latest news.

Latest News Approved - With Summaries
Upadte of Bigtoe
     posted by alalme, Wed 13 Dec 2006 01:48:39 AM UTC - 0 replies

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 - 0 replies

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 - 0 replies

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 - 0 replies

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

Verification of a new specification for the memory allocator of Topsy
     posted by alalme, Mon 07 Aug 2006 12:29:04 AM UTC - 0 replies

We have completed the verification of a new specification for the dynamic memory allocator of the Topsy operating system. The previous specification had the following inconvenient: an allocator that always fails was correct. The new specification is more
precise, it asserts that if there is enough free memory (modulo compaction), then the allocation always succeeds. The specification and its proof are in the file topsy_hmAlloc2.v.

26/05/06: simplification of the Topsy proofs
     posted by reynald, Fri 26 May 2006 02:31:08 AM UTC - 0 replies

We have made several improvements in Topsy proofs:
mainly, simplification of the assertions, and
shorter and better explained Coq scripts.

08/02/06: Topsy Heap Manager verification completed
     posted by alalme, Wed 08 Feb 2006 06:34:58 AM UTC - 0 replies

The verification of the library used by the Topsy operating system for memory allocation is completed. It includes:
1) the hmInit function: the version in topsy_hmInit.v is manual,
the version in topsy_hmInit_frag.v is semi-automatic (it relies in the decision procedure in frag.v)
2) the hmAlloc function: the version in topsy_hmAlloc.v is the same as in [Marti et al., SPACE 2006]), we are currently working on more precise specifications
3) the hmFree function (in topsy_hmFree.v)

31/01/06: simplification of the heap interface
     posted by reynald, Tue 31 Jan 2006 09:42:05 AM UTC - 0 replies

Replacement of the "heap.equal" equality with Coq equality in the interface, and simplification of related lemmas throughout the core library.

27/01/06:Decision procedure complete
     posted by alalme, Thu 26 Jan 2006 08:52:17 AM UTC - 0 replies

The decision procedure for a fragment of separation logic (located in frag.v) is now complete and axiom free. The file also contains two examples:

  *) a swap of two cells values
  *) a verification of the initialization function of the Topsy  operating system heap manager

17/01/06: module store extended with extensionality
     posted by reynald, Tue 17 Jan 2006 04:59:00 AM UTC - 0 replies

This extension required a slight change of the module interface.
The core framework has been updated to cope with this change.
Topsy proofs are still temporarily broken.

Older News Approved

Back to the top

Powered by Savane 3.9