Why CosyVerif ?
The development of CosyVerif has been decided and it is supported by three partners of the Parisian verification group, MeFoSyLoMa, which is composed of seven teams. The founding members of CosyVerif are LMF, LIP6, and LIPN.
First, these members aim at sharing their tools, comparing and supporting industrial case studies and finally making them long-lasting. Second, they also want to promote the practice of formal verification in industry and thus they intend to ease the task of integration of new formalisms and tools.
Managing CosyVerif
CosyVerif is managed by a steering committee consisting of researchers and engineers. It decides strategic orientations as well as technical choices.
Current Tools
CosyVerif is designed to support any graph-based formalism. Some examples of these formalisms are: attack-defense trees, automata, and Petri nets.
With respect to verification tools, for instance, CosyVerif performs structural analyses on Petri nets like invariant computations while other tools perform behavioural analyses: symbolic reachability graph building, unfolding, stochastic simulations, etc. Finally some of them transform high-level nets into low-level ones.
Software Status
All the developed software are open source and free software tools.
Alligator is published under the GNU Affero General Public License (AGPL), version 3.
CosyDraw is published under the GNU General Public License (GPL), version 3.
