[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Savannah-register-public] [task #5045] Submission of Separation Logic i

From: Reynald Affeldt
Subject: [Savannah-register-public] [task #5045] Submission of Separation Logic in Coq
Date: Fri, 16 Dec 2005 02:38:51 +0000
User-agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.10) Gecko/20050925 Firefox/1.0.4 (Debian package 1.0.4-2sarge5)

Follow-up Comment #2, task #5045 (project administration):

This project is essentially a library for formal verification of low-level
software based on public research results (see You can find the
current version of the implementation at the following address: It is entirely based on the
Coq proof assistant and its standard library that are distributed under the
LGPL license (see for more details). Among the examples,
we use parts of the source of the Topsy operating system that is distributed
under the GPL license (see for more details).


Reply to this item at:


  Message sent via/by Savannah

reply via email to

[Prev in Thread] Current Thread [Next in Thread]