newsBRILLANT - News: CSP||B tool for calculating control loop invariants

 
 
Show feedback again
Latest News
B parsing is complete posted by scolin, Mon Apr 16 16:22:19 2012 - 0 replies
CSP||B tool for calculating control loop invariants posted by scolin, Mon Nov 30 18:01:23 2009 - 0 replies
BiCoax, a Coq library for B, is in the repository posted by scolin, Tue Sep 2 14:54:50 2008 - 0 replies
Alpha (debian) package : brillant-core posted by gmariano, Tue Jan 29 11:57:45 2008 - 1 reply

CSP||B tool for calculating control loop invariants

Item posted by Samuel Colin <scolin> on Mon Nov 30 18:01:23 2009.

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 my (Samuel Colin) request, I saw that he used parts of BCaml for his tool. I thus added it to the BCaml sources, made some changes so as it compiles, removed the redundant files by linking to the BCaml core and made some more minor changes.

Many thanks go to Huu Nghia Nguyen, his supervisor Jean-Pierre Jacquot and the Dedale team for making this work available !

Comments:

No messages in CSP||B tool for calculating control loop invariants

 

Start a New Thread:

You could post if you were logged in
Show feedback again

Back to the top


Powered by Savane 3.1-cleanup