taskSavannah Administration - Tasks: task #5045, Submission of Separation Logic in...

 
 

task #5045: Submission of Separation Logic in Coq

Submitter:  Reynald Affeldt <reynald>
Submitted:  Thu 15 Dec 2005 02:00:41 AM UTC
   
 
Should Start On:  Thu 15 Dec 2005 12:00:00 AM UTC Should be Finished on:  Sun 25 Dec 2005 12:00:00 AM UTC
Category:  Project Approval Priority:  * 5 - Normal
Status:  Done Privacy:  Public
Assigned to:  kickino Open/Closed:  Closed
* Mandatory Fields

Add a New Comment Rich Markup
   

Jump to the original submission

Tue 03 Jan 2006 03:04:10 PM UTC, comment #7: 

Hi,

I have approved your project.  You will receive an automated e-mail containing detailed information about the approval.

Regards.

Sebastian Wieseler <kickino>
Tue 27 Dec 2005 05:53:45 AM UTC, comment #6: 

All required changes done.

rei

Reynald Affeldt <reynald>
Sat 24 Dec 2005 09:08:59 PM UTC, comment #5: 

Hello.

The address of the FSF has changed, and is now:

  51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA

Please update your license notices.

Then pleaase include an updates versions of the GPL, LGPL and GFDL into your project, which can also be found at:
http://www.gnu.org/licenses/gpl.txt
http://www.gnu.org/licenses/lgpl.txt
http://www.gnu.org/licenses/fdl.txt

Please update the copy of the license (usually, the 'COPYING' file) in your package as well.

You can find some background and a possible migration script at https://savannah.gnu.org/forum/forum.php?forum_id=3766


Have a nice weekend - the Savannah Administration

Sebastian Wieseler <kickino>
Fri 23 Dec 2005 01:34:51 AM UTC, comment #4: 
Reynald Affeldt <reynald>
Thu 22 Dec 2005 06:33:37 PM UTC, comment #3: 

Hello and sorry for the delay. Can you please provide us with a tarball of your source code? Thanks.

Sebastian Wieseler <kickino>
Fri 16 Dec 2005 02:38:51 AM UTC, comment #2: 

This project is essentially a library for formal verification of low-level software based on public research results (see http://www.dcs.qmul.ac.uk/~ohearn/localreasoning.html). You can find the current version of the implementation at the following address: http://web.yl.is.s.u-tokyo.ac.jp/~affeldt/seplog. It is entirely based on the Coq proof assistant and its standard library that are distributed under the LGPL license (see http://coq.inria.fr 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 http://www.topsy.net for more details).

Reynald Affeldt <reynald>
Thu 15 Dec 2005 07:54:10 PM UTC, comment #1: 

Hi,
I'm evaluating the project you submitted for approval in Savannah.


We need a detailed technical description that specifies such requirements as programming languages and external libraries.
It should be at least one-half a page.


Then please include a (perhaps temporary) URL pointing to the source code.
The description you gave when registering will not be read by the general public.
If you are still concerned with privacy, however, you can forward the code to me by email.

We wish to review your source code, even if it is not functional, to catch potential legal issues early.

For example, to release your program properly under the GPL you must include a copyright notice and
permission-to-copy statements at the beginning of every file of source code.  This is explained in
http://www.gnu.org/licenses/gpl-howto.html.  Our review would help catch potential omissions such as these.

Regards,

Sebastian Wieseler <kickino>
Thu 15 Dec 2005 02:00:41 AM UTC, original submission:  

A new project has been registered at Savannah
The project account will remain inactive until a site admin approve or discard the registration.


######### REGISTRATION ADMINISTRATION #########

While this item will be useful to track the registration process, approving or discarding the registration must be done using the specific "Group Administration" page, accessible only to site administrators, effectively logged as site administrators (superuser):

  <https://savannah.gnu.org/admin/groupedit.php?group_id=8196>


######### REGISTRATION DETAILS #########

Full Name:
----------
  Separation Logic in Coq

System Group Name:
-----------------
  seplog

Type:
-----
  non-GNU software & documentation

License:
--------
  GNU General Public License V2 or later

Description:
------------
  Seplog is an implementation of separation logic (an extension of Hoare
logic by John C. Reynolds, Peter W. O'Hearn, and colleagues) in the
Coq proof assistant (version 8, http://coq.inria.fr) together with a
sample verification of the heap manager of the Topsy operating system
(version 2, http://www.topsy.net). More information is available at
http://web.yl.is.s.u-tokyo.ac.jp/~affeldt/seplog.


Reynald Affeldt <reynald>

 

(Note: upload size limit is set to 16384 kB, after insertion of the required escape characters.)

Attach Files:
   
   
Comment:
   

No files currently attached

 

Depends on the following items: None found

Items that depend on this one: None found

 

CC list is empty

 

There are 0 votes so far. Votes easily highlight which items people would like to see resolved in priority, independently of the priority of the item set by tracker managers.

Only logged-in users can vote.

 

Follow 5 latest changes.

Date Changed by Updated Field Previous Value => Replaced by
2006-01-03 kickino StatusWait reply Done
    Open/ClosedOpen Closed
2005-12-24 kickino StatusNeed Info Wait reply
2005-12-15 kickino StatusNone Need Info
    Assigned toNone kickino

Back to the top

Powered by Savane 3.13-758e.
Corresponding source code