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

[Reynald Affeldt]

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


    _______________________________________________________

Reply to this item at:

  <http://savannah.gnu.org/task/?func=detailitem&item_id=5045>

_______________________________________________
  Message sent via/by Savannah
  http://savannah.gnu.org/