mainBRILLANT - Summary

 
 
Show feedback again
Membership Info
Project Admins:
7 active members

Group identification
Id: #328
System Name: brillant
Name: BRILLANT
Group Type: Programs

Search in this Group

in
   

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

 

Latest News 
B parsing is complete
     posted by scolin, Mon 16 Apr 2012 04:22:19 PM UTC - 0 replies

As of the last few months, the bparser of BCaml was modified. The end result is that we have a B grammar without any shift/reduce of reduce/reduce conflict.

Although the grammar is not as restrictive as it should be for e.g. B implementations, the parser should now work for correct B machines of any existing B project.

CSP||B tool for calculating control loop invariants
     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]
BiCoax, a Coq library for B, is in the repository
     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]
Alpha (debian) package : brillant-core
     posted by gmariano, Tue 29 Jan 2008 11:57:45 AM UTC - 1 reply

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]
[Submit News]
[13 news in archive]

Communication Tools
Mailing Lists Mailing Lists (2 public mailing-lists)

Show feedback again

Back to the top


Powered by Savane 3.1-cleanup