BRILLANT - Summary
B :
R echerches et
I nnovations
L ogicielles à
L '
A ide de
N ouvelles
T echnologies
(B : research and software innovations with the help of new technologies)
Wiki : http://vda-wikis.inrets.fr/index.ph...
RSS : http://vda-wikis.inrets.fr/index.ph...
Logo : Logo BRILLANT
Salon/chatroom jabber : brillant@chat.jabberfr.org
Archives jabber : http://chat.jabberfr.org/logs/brill...
Registration Date: Saturday 03/06/2004 at 11:52 CET
License: GNU Lesser General Public License
Development Status: 3 - Alpha
posted by scolin, Monday 11/30/2009 at 19:01 CET - 0 replies
Added as of today to the extension tools of Brillant/BCaml, a tool developed by Huu Nghia Nguyen from the LORIA/Dedale team for his internship.
For the theory behind, take a look at http://csp-b.org/
In practice, after receiving the source at ...
[Read more]
posted by scolin, Tuesday 09/02/2008 at 16:54 CEST - 0 replies
Coq libraries for B have entered the BRILLANT project under the BiCoax name. These libraries are meant as a future replacement for BPhoX, as PhoX is not maintained anymore: this seems a good excuse to transfer BPhoX knowledge to Coq, whose longevity is more ensured.
...
[Read more]
posted by gmariano, Tuesday 01/29/2008 at 12:57 CET - 0 replies
A new (debian) package is available in the download area.
It is still in alpha stage but provides a small set of B tools (parser, proof obligation generator, xsl transformation,...) and uses the phox prover to discharge proof obligations.
...
[Read more]
posted by scolin, Monday 01/28/2008 at 17:51 CET - 0 replies
We moved the jabber chatroom to:
brillant@chat.jabberfr.org
so as to get logs of the discussions, available here:
http://chat.jabberfr.org/logs/brill...
####
Le salon de discussion est déplacé vers:
...
[Read more]
Mailing Lists (2 public mailing-lists)
