Presentation

From BWare
Jump to: navigation, search
Line 4: Line 4:
 
and requiring high guarantees of confidence. It therefore addresses Topic 1
 
and requiring high guarantees of confidence. It therefore addresses Topic 1
 
(``''Sécurité des systèmes numériques''<nowiki>''</nowiki>) and Topic 2 (``''Ingénierie du logiciel et du matériel''<nowiki>''</nowiki>)
 
(``''Sécurité des systèmes numériques''<nowiki>''</nowiki>) and Topic 2 (``''Ingénierie du logiciel et du matériel''<nowiki>''</nowiki>)
of the ``''Ingénierie Numérique & Sécurité''<nowiki>''</nowiki>
+
of the [http://www.agence-nationale-recherche.fr/ ANR] [http://www.agence-nationale-recherche.fr/INS-2012 ``''Ingénierie Numérique & Sécurité''<nowiki>''</nowiki>]
 
call.
 
call.
  
Line 30: Line 30:
 
obligations for the B method; translation from set theory to first-order
 
obligations for the B method; translation from set theory to first-order
 
logic; automated theorem proving; proof production and proof checking. The
 
logic; automated theorem proving; proof production and proof checking. The
BWare consortium associates academics entities (Cedric, Lri, and
+
BWare consortium associates academics entities ([http://cedric.cnam.fr Cedric], [http://www.lri.fr/ Lri], and
Inria) and industrial partners (Mitsubishi Electric R&D Centre Europe, ClearSy, and OCamlPro). This
+
[http://www.inria.fr/ Inria]) and industrial partners ([http://www.mitsubishielectric-rce.eu/ Mitsubishi Electric R&D Centre Europe], [http://www.clearsy.com/ ClearSy], and
 +
[http://www.ocamlpro.com/ OCamlPro]). This
 
will ensure an excellent level of expertise for the scientific aspects as well
 
will ensure an excellent level of expertise for the scientific aspects as well
 
as their exploitation for the development of software with high guarantees of
 
as their exploitation for the development of software with high guarantees of
Line 42: Line 43:
 
design of a verification platform, which will gather several tools, and some
 
design of a verification platform, which will gather several tools, and some
 
extensions of these tools will be considered and developed. This platform will
 
extensions of these tools will be considered and developed. This platform will
be integrated to the tool of an industrial partner (Atelier B from ClearSy)
+
be integrated to the tool of an industrial partner ([http://www.atelierb.eu/ Atelier B] from ClearSy)
 
for evaluation over industrial applications and comparison with other similar
 
for evaluation over industrial applications and comparison with other similar
 
existing verification tools. An activity of interactive proof will be also
 
existing verification tools. An activity of interactive proof will be also

Revision as of 00:44, 3 October 2012

Personal tools
Namespaces

Variants
Actions
Navigation
Toolbox