460:, which consists of deciding whether or not the system model satisfies the logical properties. CADP contains model checking tools for a powerful form of temporal logic, the modal mu-calculus, which is extended with typed variables and expressions so as to express predicates over the data contained in the model. This extension provides for properties that could not be expressed in the standard mu-calculus (for instance, the fact that the value of a given variable is always increasing along any execution path).
449:, which consists in comparing the system model and its properties (both represented as automata) modulo some equivalence or preorder relation. CADP contains equivalence checking tools that compare and minimize automata modulo various equivalence and preorder relations; some of these tools also apply to stochastic and probabilistic models (such as Markov chains). CADP also contains
175:
Models provide mathematical representations for parallel programs and related verification problems. Examples of models are automata, networks of communicating automata, Petri nets, binary decision diagrams, boolean equation systems, etc. From a theoretical point of view, research on models seeks for
687:
The CADP tools are well-integrated and can be accessed easily using either the EUCALYPTUS graphical interface or the SVL scripting language. Both EUCALYPTUS and SVL provide users with an easy, uniform access to the CADP tools by performing file format conversions automatically whenever needed and by
537:
OPEN/CAESAR is a generic software environment for developing tools that explore graphs on the fly (for instance, simulation, verification, and test generation tools). Such tools can be developed independently of any particular high level language. In this respect, OPEN/CAESAR plays a central role in
533:
CAESAR is a compiler that translates LOTOS processes into either C code (for rapid prototyping and testing purposes) or finite graphs (for verification). The translation is done using several intermediate steps, among which the construction of a Petri net extended with typed variables, data handling
512:
CADP is distributed free of charge to universities and public research centers. Users in industry can obtain an evaluation license for non-commercial use during a limited period of time, after which a full license is required. To request a copy of CADP, complete the registration form at. After the
603:
BCG (Binary Coded Graphs) is both a file format for storing very large graphs on disk (using efficient compression techniques) and a software environment for handling this format, including partitioning graphs for distributed processing. BCG also plays a key role in CADP as many tools rely on this
439:
Most of the verification algorithms in CADP are based on the labeled transition systems (or, simply, automata or graphs) model, which consists of a set of states, an initial state, and a transition relation between states. This model is often generated automatically from high level descriptions of
649:
XTL (eXecutable
Temporal Language), which is a high level, functional language for programming exploration algorithms on BCG graphs. XTL provides primitives to handle states, transitions, labels, successor and predecessor functions, etc. For instance, one can define recursive functions on sets of
481:
Accurate specification of reliable, complex systems requires a language that is executable (for enumerative verification) and has formal semantics (to avoid any as language ambiguities that could lead to interpretation divergences between designers and implementors). Formal semantics are also
167:
CADP can be applied to any system that comprises asynchronous concurrency, i.e., any system whose behavior can be modeled as a set of parallel processes governed by interleaving semantics. Therefore, CADP can be used to design hardware architecture, distributed algorithms, telecommunications
500:
LOTOS was heavily revised in 2001, leading to the publication of E-LOTOS (Enhanced-Lotos, ISO/IEC standard 15437:2001), which tries to provide a greater expressiveness (for instance, by introducing quantitative time to describe systems with real-time constraints) together with a better user
482:
required when it is necessary to establish the correctness of an infinite system; this cannot be done using enumerative techniques because they deal only with finite abstractions, so must be done using theorem proving techniques, which only apply to languages with a formal semantics.
427:
CADP is designed in a modular way and puts the emphasis on intermediate formats and programming interfaces (such as the BCG and OPEN/CAESAR software environments), which allow the CADP tools to be combined with other tools and adapted to various specification languages.
464:
Although these techniques are efficient and automated, their main limitation is the state explosion problem, which occurs when models are too large to fit in computer memory. CADP provides software technologies for handling models in two complementary ways:
168:
protocols, etc. The enumerative verification (also known as explicit state verification) techniques implemented in CADP, though less general that theorem proving, enable an automatic, cost-efficient detection of design errors in complex systems.
857:, in Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'98 (Lisbon, Portugal), Berlin, B. Steffen (editor), Lecture Notes in Computer Science, Full version available as
737:
In 2021, Hubert
Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe jointly won the Innovation Prize of Inria – Académie des sciences – Dassault Systèmes for their scientific work that led to the development of the CADP
731:
In 2020, Frédéric Lang, Franco
Mazzanti, and Wendelin Serwe won three gold medals at the RERS'2020 challenge by correctly solving 88% of the "Parallel CTL" problems, only giving "don't know" answers for 11 formulas out of
444:
Behavioral properties express the intended functioning of the system in the form of automata (or higher level descriptions, which are then translated into automata). In such a case, the natural approach to verification is
24:
415:
Several verification algorithms combined: enumerative verification, on-the-fly verification, symbolic verification using binary decision diagrams, compositional minimization, partial orders, distributed model checking,
529:
abstract data types into C types and C functions. The translation involves pattern-matching compiling techniques and automatic recognition of usual types (integers, enumerations, tuples, etc.), which are implemented
683:
The CADP toolbox also includes additional tools, such as ALDEBARAN and TGV (Test
Generation based on Verification) developed by the Verimag laboratory (Grenoble) and the Vertecs project-team of INRIA Rennes.
744:
436:
Verification is comparison of a complex system against a set of properties characterizing the intended functioning of the system (for instance, deadlock freedom, mutual exclusion, fairness, etc.).
440:
the system under study, then compared against the system properties using various decision procedures. Depending on the formalism used to express the properties, two approaches are possible:
489:
description of the system. LOTOS is an international standard for protocol description (ISO/IEC standard 8807:1989), which combines the concepts of process algebras (in particular
216:
The releases of CADP have been successively named with alphabetic letters (from "A" to "Z"), then with the names of cities hosting academic research groups actively working on the
718:
In 2019, Frédéric Lang and Franco
Mazzanti won all the gold medals for the parallel problems of the RERS challenge by using CADP to successfully and correctly evaluate 360
400:
Networks of communicating automata, i.e., finite state machines running in parallel and synchronized (either using process algebra operators or synchronization vectors).
394:. The toolbox contains two compilers (CAESAR and CAESAR.ADT) that translate LOTOS descriptions into C code to be used for simulation, verification, and testing purposes.
538:
CADP by connecting language-oriented tools with model-oriented tools. OPEN/CAESAR consists of a set of 16 code libraries with their programming interfaces, such as:
196:
Work began on CADP in 1986, when the development of the first two tools, CAESAR and ALDEBARAN, was undertaken. In 1989, the CADP acronym was coined, which stood for
160:
The purpose of the CADP toolkit is to facilitate the design of reliable systems by use of formal description techniques together with software tools for simulation,
504:
Several tools exist to convert descriptions in other process calculi or intermediate format into LOTOS, so that the CADP tools can then be used for verification.
456:
Logical properties express the intended functioning of the system in the form of temporal logic formulas. In such a case, the natural approach to verification is
656:
The connection between explicit models (such as BCG graphs) and implicit models (explored on the fly) is ensured by OPEN/CAESAR-compliant compilers including:
743:
In 2023, Hubert
Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe jointly received, for the CADP toolbox, the first ever Test-of-Time Tool Award from
179:
In practice, models are often too elementary to describe complex systems directly (this would be tedious and error-prone). A higher level formalism known as
958:
704:
of CADP, received the
Information Technology Award attributed during the 10th edition of the yearly symposium organized by the Foundation RhĂ´ne-Alpes Futur.
796:
650:
states, which allow to specify in XTL evaluation and diagnostic generation fixed point algorithms for usual temporal logics (such as HML, CTL, ACTL, etc.).
526:
486:
391:
217:
1018:
153:) is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the CONVECS team (formerly by the VASY team) at
604:
format for their inputs/outputs. The BCG environment consists of various libraries with their programming interfaces, and of several tools, including:
472:
Larger models are represented implicitly, by exploring only the model states and transitions needed for the verification (on the fly verification).
367:
Between major releases, minor releases are often available, providing early access to new features and improvements. For more information, see the
1122:
1117:
204:. Currently CADP contains over 50 tools. While keeping the same acronym, the name of the toolbox has been changed to better indicate its purpose:
200:. Over time, several tools were added, including programming interfaces that enabled tools to be contributed: the CADP acronym then became the
157:
Rhone-Alpes and connected to various complementary tools. CADP is maintained, regularly improved, and used in many industrial projects.
628:
BCG_MIN, which minimizes a graph modulo strong or branching equivalences (and can also deal with probabilistic and stochastic systems)
494:
187:
is needed for this task, as well as compilers that translate high-level descriptions into models suitable for verification algorithms.
490:
927:
Proceedings of the 21st IFIP WG 6.1 International
Conference on Formal Techniques for Networked and Distributed Systems FORTE'2001
497:
and algebraic abstract data types. Thus, LOTOS can describe both asynchronous concurrent processes and complex data structures.
171:
CADP includes tools to support use of two approaches in formal methods, both of which are needed for reliable systems design:
469:
Small models can be represented explicitly, by storing in memory all their states and transitions (exhaustive verification);
161:
1127:
63:
1046:
106:
962:
710:
1132:
1107:
719:
1112:
1102:
844:(Ottawa, Canada), L. Logrippo, R. L. Probert, H. Ural (editors), North-Holland, IFIP, June 1990, p. 379–394.
592:
REDUCTOR, which constructs and minimizes the graph of reachable states modulo various equivalence relations
782:
723:
568:
DETERMINATOR, which eliminates stochastic nondeterminism in normal, probabilistic, or stochastic systems
634:
BCG_TRANSIENT, which performs transient numerical analysis of (extended) continuous-time Markov chains
631:
BCG_STEADY, which performs steady-state numerical analysis of (extended) continuous-time Markov chains
379:
CADP offers a wide set of functionalities, ranging from step-by-step simulation to massively parallel
450:
446:
420:
406:
409:
tools (minimization and comparisons modulo bisimulation relations), such as BCG_MIN and BISIMULATOR.
842:
Proceedings of the 10th
International Symposium on Protocol Specification, Testing and Verification
622:
BCG_LABELS, which hides and/or renames (using regular expressions) the transition labels of a graph
117:
513:
license agreement has been signed, you will receive details of how to download and install CADP.
221:
787:
International
Journal on Software Tools for Technology Transfer (STTT), 15(2):89-107, April 2013
929:(Cheju Island, Korea), M. Kim, B. Chin, S. Kang, D. Lee (editors), Full version available as
889:
Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications
412:
Several model-checkers for various temporal logic and mu-calculus, such as EVALUATOR and XTL.
184:
89:
180:
827:(Vancouver B.C., Canada), S. T. Vuong (editor), North-Holland, December 1989, p. 147–162.
825:
Proceedings of the 2nd International Conference on Formal Description Techniques FORTE'89
1004:
976:
457:
380:
1096:
701:
625:
BCG_MERGE, which gathers graph fragments obtained from distributed graph construction
580:
EXHIBITOR, which searches for execution sequences matching a given regular expression
122:
855:
OPEN/CÆSAR: An Open Software Architecture for Verification, Simulation, and Testing
610:
BCG_EDIT which allows to modify interactively the graph layout produced by Bcg_Draw
220:
language and, more generally, the names of cities in which major contributions to
571:
DISTRIBUTOR, which generates the graph of reachable states using several machines
709:
In 2011, Hubert Garavel, software architect and developer of CADP, received the
110:
784:
CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes
1032:
31:
1060:
943:
619:
BCG_IO, which performs conversions between BCG and many other graph formats
556:
A number of tools have been developed within the OPEN/CAESAR environment:
453:
tools that can be used to verify a graphical representation of the system.
1019:"CNR-Inria Team Wins Gold Medals at the RERS 2020 Parallel CTL Challenge"
944:"Radu Mateescu wins the IT Award granted by Fondation RhĂ´ne-Alpes Futur"
574:
EVALUATOR, which evaluates regular alternation-free mu-calculus formulas
547:
Caesar_Stack, which implements stacks for depth-first search exploration
550:
Caesar_Table, which handles tables of states, transitions, labels, etc.
94:
616:
BCG_INFO, which displays various statistical information about a graph
23:
930:
858:
807:
757:
688:
supplying appropriate command-line options as the tools are invoked.
613:
BCG_GRAPH, which generates various forms of practically useful graphs
123:
Toolbox for designing communication protocols and distributed systems
990:
368:
176:
general results, independent of any particular description language.
595:
SIMULATOR, X-SIMULATOR and OCIS, which allow interactive simulation
397:
Low-level protocol descriptions specified as finite state machines.
640:
PBG_INFO, which displays information about a partitioned BCG graph
586:
PREDICTOR, which predict the feasibility of reachability analysis,
154:
102:
98:
36:
700:
In 2002, Radu Mateescu, who designed and developed the EVALUATOR
562:
BISIMULATOR, which checks bisimulation equivalences and preorders
959:"Hubert Garavel received the Gay-Lussac Humboldt Research Award"
761:
544:
Caesar_Solve, which resolves boolean equation systems on the fly
1047:"The Convecs team strengthens the security of parallel systems"
726:(LTL) formulas on various sets of communicating state machines.
589:
PROJECTOR, which computes abstractions of communicating systems
390:
High-level protocol descriptions written in the ISO language
933:, Kluwer Academic Publishers, IFIP, August 2001, p. 377–392.
677:
SEQ.OPEN, for models represented as sets of execution traces
565:
CUNCTATOR, which performs on-the-fly steady state simulation
1087:
39:
607:
BCG_DRAW, which builds a two-dimensional view of a graph,
583:
GENERATOR, which constructs the graph of reachable states
1082:
1077:
923:
SVL: a Scripting Language for Compositional Verification
668:
EXP.OPEN, for models expressed as communicating automata
906:
Action versus State Based Logics for Transition Systems
662:
CAESAR.OPEN, for models expressed as LOTOS descriptions
419:
Plus other tools with advanced functionalities such as
133:
43:
810:. Cadp.inria.fr (2011-08-30). Retrieved on 2014-06-16.
893:
ACM Transactions on Programming Languages and Systems
797:
ISO 8807, Language of Temporal Ordering Specification
838:
Compilation and Verification of LOTOS Specifications
861:, Springer Verlag, March 1998, vol. 1384, p. 68–84.
128:
116:
88:
62:
50:
30:
747:, the premier European forum for software science.
674:LNT.OPEN, for models expressed as LNT descriptions
671:FSP.OPEN, for models expressed as FSP descriptions
541:Caesar_Hash, which contains several hash functions
206:Construction and Analysis of Distributed Processes
151:Construction and Analysis of Distributed Processes
17:Construction and Analysis of Distributed Processes
872:Algebraic Laws for Nondeterminism and Concurrency
577:EXECUTOR, which performs random execution of code
1033:"The CADP Newsletter Nr. 13 - February 22, 2021"
912:, Springer Verlag, 1990, vol. 469, p. 407–419.
665:BCG.OPEN, for models represented as BCG graphs
598:TERMINATOR, which searches for deadlock states
991:"The CADP Newsletter Nr. 12 - April 10, 2019"
646:PBG_RM, which removes a partitioned BCG graph
8:
637:PBG_CP, which copies a partitioned BCG graph
16:
887:E. M. Clarke, E. A. Emerson, A. P. Sistla.
643:PBG_MV which moves a partitioned BCG graph
22:
15:
525:CAESAR.ADT is a compiler that translates
821:Compilation of LOTOS Abstract Data Types
781:Garavel H, Lang F, Mateescu R, Serwe W:
387:Compilers for several input formalisms:
226:
895:, April 1986, vol. 8, no 2, p. 244–263.
774:
760:compiler generator (used to build many
198:CAESAR/ALDEBARAN Distribution Package
164:, verification, and test generation.
7:
1005:"Results of the RERS Challenge 2020"
977:"Results of the RERS Challenge 2019"
521:The toolbox contains several tools:
477:Languages and compilation techniques
202:CAESAR/ALDEBARAN Development Package
432:Models and verification techniques
14:
957:Isabelle Bellin (16 April 2011).
910:Lecture Notes in Computer Science
534:features, and atomic transitions.
904:R. De Nicola, F. W. Vaandrager.
69:2023 / February 13, 2023
1061:"ETAPS Test-of-Time Tool Award"
1123:Concurrency (computer science)
1118:Formal specification languages
423:, performance evaluation, etc.
1:
931:Inria Research Report RR-4223
859:Inria Research Report RR-3352
241:January 1990 - December 1996
162:rapid application development
878:, 1985, vol. 32, p. 137–161.
54:1989, 34–35 years ago
1149:
764:compilers and translators)
508:Licensing and installation
371:page on the CADP website.
711:Gay-Lussac Humboldt Prize
84:
58:
21:
1088:http://convecs.inria.fr/
870:M. Hennessy, R. Milner.
836:H. Garavel, J. Sifakis.
808:CADP Online Request Form
720:computational tree logic
71:; 18 months ago
1083:http://vasy.inria.fr/
1078:http://cadp.inria.fr/
921:H. Garavel, F. Lang.
724:linear temporal logic
447:equivalence checking
407:equivalence checking
1128:Concurrency control
18:
876:Journal of the ACM
222:concurrency theory
365:
364:
310:Sophia Antipolis
144:
143:
1140:
1065:
1064:
1057:
1051:
1050:
1043:
1037:
1036:
1029:
1023:
1022:
1015:
1009:
1008:
1001:
995:
994:
987:
981:
980:
973:
967:
966:
961:. Archived from
954:
948:
947:
940:
934:
919:
913:
902:
896:
885:
879:
868:
862:
851:
845:
834:
828:
817:
811:
805:
799:
794:
788:
779:
227:
224:have been made.
185:process calculus
140:
137:
135:
90:Operating system
79:
77:
72:
26:
19:
1148:
1147:
1143:
1142:
1141:
1139:
1138:
1137:
1133:Synchronization
1108:Process calculi
1093:
1092:
1074:
1069:
1068:
1059:
1058:
1054:
1045:
1044:
1040:
1031:
1030:
1026:
1017:
1016:
1012:
1003:
1002:
998:
989:
988:
984:
975:
974:
970:
956:
955:
951:
942:
941:
937:
920:
916:
903:
899:
886:
882:
869:
865:
852:
848:
835:
831:
818:
814:
806:
802:
795:
791:
780:
776:
771:
754:
697:
691:
519:
510:
485:CADP acts on a
479:
451:visual checking
434:
421:visual checking
383:. It includes:
377:
214:
194:
181:process algebra
132:
80:
75:
73:
70:
51:Initial release
42:team (formerly
12:
11:
5:
1146:
1144:
1136:
1135:
1130:
1125:
1120:
1115:
1113:Formal methods
1110:
1105:
1103:Model checkers
1095:
1094:
1091:
1090:
1085:
1080:
1073:
1072:External links
1070:
1067:
1066:
1052:
1038:
1024:
1010:
996:
982:
968:
965:on 2016-07-10.
949:
935:
914:
897:
880:
863:
846:
829:
812:
800:
789:
773:
772:
770:
767:
766:
765:
753:
750:
749:
748:
740:
739:
734:
733:
728:
727:
715:
714:
706:
705:
696:
693:
681:
680:
679:
678:
675:
672:
669:
666:
663:
654:
653:
652:
651:
647:
644:
641:
638:
635:
632:
629:
626:
623:
620:
617:
614:
611:
608:
601:
600:
599:
596:
593:
590:
587:
584:
581:
578:
575:
572:
569:
566:
563:
554:
553:
552:
551:
548:
545:
542:
535:
531:
518:
515:
509:
506:
501:friendliness.
478:
475:
474:
473:
470:
462:
461:
458:model checking
454:
433:
430:
425:
424:
417:
413:
410:
403:
402:
401:
398:
395:
381:model checking
376:
373:
363:
362:
361:February 2023
359:
355:
354:
353:December 2022
351:
347:
346:
345:December 2021
343:
339:
338:
337:December 2020
335:
331:
330:
329:December 2019
327:
323:
322:
321:December 2018
319:
315:
314:
313:December 2017
311:
307:
306:
305:December 2016
303:
299:
298:
297:December 2015
295:
291:
290:
289:December 2014
287:
283:
282:
281:December 2013
279:
275:
274:
273:December 2006
271:
267:
266:
263:
259:
258:
255:
251:
250:
247:
243:
242:
239:
235:
234:
231:
213:
212:Major releases
210:
193:
190:
189:
188:
177:
142:
141:
130:
126:
125:
120:
114:
113:
92:
86:
85:
82:
81:
68:
66:
64:Stable release
60:
59:
56:
55:
52:
48:
47:
34:
28:
27:
13:
10:
9:
6:
4:
3:
2:
1145:
1134:
1131:
1129:
1126:
1124:
1121:
1119:
1116:
1114:
1111:
1109:
1106:
1104:
1101:
1100:
1098:
1089:
1086:
1084:
1081:
1079:
1076:
1075:
1071:
1062:
1056:
1053:
1048:
1042:
1039:
1034:
1028:
1025:
1020:
1014:
1011:
1006:
1000:
997:
992:
986:
983:
978:
972:
969:
964:
960:
953:
950:
945:
939:
936:
932:
928:
924:
918:
915:
911:
907:
901:
898:
894:
890:
884:
881:
877:
873:
867:
864:
860:
856:
850:
847:
843:
839:
833:
830:
826:
822:
816:
813:
809:
804:
801:
798:
793:
790:
786:
785:
778:
775:
768:
763:
759:
756:
755:
751:
746:
742:
741:
736:
735:
730:
729:
725:
721:
717:
716:
712:
708:
707:
703:
702:model checker
699:
698:
694:
692:
689:
685:
676:
673:
670:
667:
664:
661:
660:
659:
658:
657:
648:
645:
642:
639:
636:
633:
630:
627:
624:
621:
618:
615:
612:
609:
606:
605:
602:
597:
594:
591:
588:
585:
582:
579:
576:
573:
570:
567:
564:
561:
560:
559:
558:
557:
549:
546:
543:
540:
539:
536:
532:
528:
524:
523:
522:
517:Tools summary
516:
514:
507:
505:
502:
498:
496:
492:
488:
483:
476:
471:
468:
467:
466:
459:
455:
452:
448:
443:
442:
441:
437:
431:
429:
422:
418:
414:
411:
408:
404:
399:
396:
393:
389:
388:
386:
385:
384:
382:
375:CADP features
374:
372:
370:
360:
357:
356:
352:
349:
348:
344:
342:Saarbruecken
341:
340:
336:
333:
332:
328:
325:
324:
320:
317:
316:
312:
309:
308:
304:
301:
300:
296:
293:
292:
288:
285:
284:
280:
277:
276:
272:
269:
268:
264:
261:
260:
257:January 1999
256:
253:
252:
248:
245:
244:
240:
237:
236:
232:
229:
228:
225:
223:
219:
211:
209:
207:
203:
199:
191:
186:
182:
178:
174:
173:
172:
169:
165:
163:
158:
156:
152:
148:
139:
131:
127:
124:
121:
119:
115:
112:
108:
104:
100:
96:
93:
91:
87:
83:
67:
65:
61:
57:
53:
49:
45:
41:
38:
35:
33:
29:
25:
20:
1055:
1041:
1027:
1013:
999:
985:
971:
963:the original
952:
938:
926:
922:
917:
909:
905:
900:
892:
888:
883:
875:
871:
866:
854:
853:H. Garavel.
849:
841:
837:
832:
824:
820:
819:H. Garavel.
815:
803:
792:
783:
777:
690:
686:
682:
655:
555:
520:
511:
503:
499:
484:
480:
463:
438:
435:
426:
378:
366:
294:Stony Brook
238:"A" ... "Z"
215:
205:
201:
197:
195:
170:
166:
159:
150:
146:
145:
32:Developer(s)
369:change list
111:OpenIndiana
1097:Categories
769:References
722:(CTL) and
530:optimally.
286:Amsterdam
270:Edinburgh
265:July 2001
249:June 1997
230:Code name
76:2023-02-13
752:See also
738:toolbox.
405:Several
334:Aalborg
318:Uppsala
358:Aachen
302:Oxford
278:Zurich
262:Ottawa
246:Twente
192:History
129:Website
107:Solaris
95:Windows
74: (
40:CONVECS
925:, in:
891:, in:
874:, in:
758:SYNTAX
695:Awards
350:Kista
254:Liege
136:.inria
109:, and
840:, in
823:, in
745:ETAPS
527:LOTOS
487:LOTOS
392:LOTOS
326:Pisa
233:Date
218:LOTOS
155:INRIA
103:Linux
99:macOS
46:team)
37:INRIA
762:CADP
493:and
416:etc.
147:CADP
134:cadp
118:Type
44:VASY
732:90.
495:CSP
491:CCS
183:or
138:.fr
1099::
908:,
208:.
105:,
101:,
97:,
1063:.
1049:.
1035:.
1021:.
1007:.
993:.
979:.
946:.
713:.
149:(
78:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
