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.php/Projet_BRILLANT
RSS : http://vda-wikis.inrets.fr/index.php?title=Special:Recentchanges&feed=rss
Logo : Logo BRILLANT
Salon/chatroom jabber : brillant@chat.jabberfr.org
Archives jabber : http://chat.jabberfr.org/logs/brillant@chat.jabberfr.org/
Registration Date: Sat 06 Mar 2004 10:52:28 AM UTC
License: GNU Lesser General Public License
Development Status: 3 - Alpha
posted by scolin, Mon 30 Nov 2009 06:01:23 PM UTC - 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, Tue 02 Sep 2008 02:54:50 PM UTC - 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, Tue 29 Jan 2008 11:57:45 AM UTC - 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, Mon 28 Jan 2008 04:51:22 PM UTC - 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/brillant@chat.jabberfr.org/
####
Le salon de discussion est déplacé vers:
brillant@chat.jabberfr.org
de façon à avoir un archivage des discussions, disponibles ici:
http://chat.jabberfr.org/logs/brillant@chat.jabberfr.org/
[Submit News]
[12 news in archive]


