NEWS

CAI 2013 Conference
CLEARSY participated to CAI 2013 conference (International Conference on Algebraic Informatics) held in Porquerolles (France) 3-6 September 2013. A talk,...

Dagstuhl Seminar 2013
CLEARSY attended a Seminar,"Integration of Tools for Rigorous Software Construction and Analysis" (13372), held at Schloss Dagstuhl in Germany (8-13...

SYSTEM LEVEL FORMAL PROOFS FOR THE CBTC OF THE NEW YORK FLUSHING LINE
System level proofs for the CBTC of the New York Flushing line has been presented on June 26th 2013 in Paris. The aim of this presentation is to give the...

SuperZenon to provide another prover to Atelier B
"SuperZenon is an experimental extension of the Zenon automated theorem prover, using the principles of superdeduction, among which the theory is used to...

How to install Atelier B 4.1 on a Debian-like 64 bits machine
Atelier B 4.1 has been released in 2012. For Linux machines, it is available as a binary packages for 32 bits x86 machines in RPM and DEB format....

Formal verification of PLC programs using the B method
We pusblish this report which is related to safety critical industrial automation systems. Author: Haniel Moreira BarbosaAdvisor: David DéharbeDate: October...