{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T21:12:44Z","timestamp":1775769164633,"version":"3.50.1"},"reference-count":128,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,6,30]],"date-time":"2012-06-30T00:00:00Z","timestamp":1341014400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,4]]},"DOI":"10.1007\/s10009-012-0244-z","type":"journal-article","created":{"date-parts":[[2012,7,9]],"date-time":"2012-07-09T01:34:55Z","timestamp":1341797695000},"page":"89-107","source":"Crossref","is-referenced-by-count":219,"title":["CADP 2011: a toolbox for the construction and analysis of distributed processes"],"prefix":"10.1007","volume":"15","author":[{"given":"Hubert","family":"Garavel","sequence":"first","affiliation":[]},{"given":"Fr\u00e9d\u00e9ric","family":"Lang","sequence":"additional","affiliation":[]},{"given":"Radu","family":"Mateescu","sequence":"additional","affiliation":[]},{"given":"Wendelin","family":"Serwe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,6,30]]},"reference":[{"issue":"1","key":"244_CR1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)90266-6","volume":"126","author":"H.R. Andersen","year":"1994","unstructured":"Andersen H.R.: Model checking and boolean graphs. Theor. Comput. Sci. 126(1), 3\u201330 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"244_CR2","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u010ce\u0161ka, M., Ro\u010dkai, P.\u201d: DiVinE: parallel distributed model checker (tool paper). In: Proceedings of Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology HiBi\/PDMC 2010 (Twente, The Netherlands), pp. 4\u20137. IEEE Computer Society Press, Sept 2010","DOI":"10.1109\/PDMC-HiBi.2010.9"},{"key":"244_CR3","doi-asserted-by":"crossref","unstructured":"Belinfante, A., Feenstra, J., de Vries, R.G., Tretmans, J., Goga, N., Feijs, L., Mauw, S., Heerink, L.: Formal test automation: a simple experiment. In: Proceedings of the IFIP 12th International Workshop on Testing of Communicating Systems IWTCS\u201999 (Budapest, Hungary). Kluwer, Dordrecht, Sept 1999","DOI":"10.1007\/978-0-387-35567-2_12"},{"key":"244_CR4","doi-asserted-by":"crossref","unstructured":"Bergamini, D., Descoubes, N., Joubert, C., Mateescu, R.: BISIMULATOR: a modular tool for on-the-fly equivalence checking. In: Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS\u20192005 (Edinburgh, Scotland, UK). Lecture Notes in Computer Science, vol. 3440, pp. 581\u2013585. Springer, Berlin, April 2005","DOI":"10.1007\/978-3-540-31980-1_42"},{"key":"244_CR5","unstructured":"Berthomieu, B., Bodeveix, J.-P., Farail, P., Filali, M., Garavel, H., Gaufillet, P., Lang, F., Vernadat, F.: FIACRE: An intermediate language for model verification in the TOPCASED environment. In: Proceedings of the 4th European Congress on Embedded Real-Time Software ERTS\u201908 (Toulouse, France). SIA (the French Society of Automobile Engineers), AAAF (the French Society of Aeronautic and Aerospace), and SEE (the French Society for Electricity, Electronics, and Information & Communication Technologies), Jan 2008"},{"issue":"3","key":"244_CR6","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/s10009-004-0185-2","volume":"7","author":"S. Blom","year":"2005","unstructured":"Blom S., Orzan S.: Distributed state space minimization. Softw. Tools Technol. Transfer 7(3), 280\u2013291 (2005)","journal-title":"Softw. Tools Technol. Transfer"},{"key":"244_CR7","doi-asserted-by":"crossref","unstructured":"Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Proceedings of the 22nd International Conference on Computer Aided Verification CAV 2010 (Edinburgh, UK). Lecture Notes in Computer Science, vol. 6174, pp. 354\u2013359. Springer, Berlin, July 2010","DOI":"10.1007\/978-3-642-14295-6_31"},{"key":"244_CR8","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Fernandez, J.-C., Graf, S., Rodr\u00edguez, C., Sifakis, J.: Safety for branching time semantics. In: Proceedings of 18th ICALP. Springer, Berlin, July 1991","DOI":"10.1007\/3-540-54233-7_126"},{"key":"244_CR9","doi-asserted-by":"crossref","unstructured":"Bouali, A., Ressouche, A., Roy, V., de Simone, R.: The Fc2Tools set: a toolset for the verification of concurrent systems. In: Proceedings of the 8th Conference on Computer-Aided Verification (New Brunswick, New Jersey, USA). Lecture Notes in Computer Science, vol. 1102. Springer, Berlin, Aug 1996","DOI":"10.1007\/3-540-61474-5_98"},{"key":"244_CR10","doi-asserted-by":"crossref","unstructured":"Boyer, F., Gruber, O., Sala\u00fcn, G.: Specifying and verifying the SYNERGY reconfiguration protocol with LOTOS NT\/CADP. In: Proceedings of the 17th International Symposium on Formal Methods FM\u20192011 (Limerick, Ireland). Lecture Notes in Computer Science, vol. 6664, pp. 103\u2013117. Springer, Berlin, June 2011","DOI":"10.1007\/978-3-642-21437-0_10"},{"key":"244_CR11","doi-asserted-by":"crossref","unstructured":"Bozga, M., Fernandez, J.-C., Ghirvu, L., Graf, S., Krimm, J.-P., Mounier, L.: IF: an intermediate representation and validation environment for timed asynchronous systems. In: Proceedings of World Congress on Formal Methods in the Development of Computing Systems FM\u201999 (Toulouse, France). Springer, Berlin, Sept 1999","DOI":"10.1007\/3-540-48119-2_19"},{"issue":"3","key":"244_CR12","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"S.D. Brookes","year":"1984","unstructured":"Brookes S.D., Hoare C.A.R., Roscoe A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560\u2013599 (1984)","journal-title":"J. ACM"},{"key":"244_CR13","unstructured":"Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., McKinty, C., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4). INRIA\/VASY, Sept 2011"},{"key":"244_CR14","doi-asserted-by":"crossref","unstructured":"Chehaibar, G., Garavel, H., Mounier, L., Tawbi, N., Zulian, F.: Specification and verification of the powerscale bus arbitration protocol: an industrial experiment with LOTOS. In: Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification FORTE\/PSTV\u201996 (Kaiserslautern, Germany), pp. 435\u2013450. IFIP, Chapman & Hall, Oct 1996. Full version available as INRIA Research Report RR-2958","DOI":"10.1007\/978-0-387-35079-0_28"},{"key":"244_CR15","doi-asserted-by":"crossref","unstructured":"Chehaibar, G., Zidouni, M., Mateescu, R.: Modeling multiprocessor Cache protocol impact on MPI performance. In: Proceedings of the 2009 IEEE International Workshop on Quantitative Evaluation of Large-Scale Systems and Technologies QuEST\u201909 (Bradford, UK). IEEE Computer Society Press, May 2009","DOI":"10.1109\/WAINA.2009.117"},{"key":"244_CR16","unstructured":"Cheung, K.H.: Compositional analysis of complex distributed systems. PhD thesis, Department of Computer Science, Hong Kong University of Science and Technology, Hong Kong (1998)"},{"key":"244_CR17","doi-asserted-by":"crossref","unstructured":"Cheung, S.C., Kramer, J.: Enhancing compositional reachability analysis with context constraints. In: Proceedings of the 1st ACM SIGSOFT International Symposium on the Foundations of Software Engineering (Los Angeles, CA, USA), pp. 115\u2013125. ACM Press, Dec 1993","DOI":"10.1145\/256428.167071"},{"key":"244_CR18","doi-asserted-by":"crossref","unstructured":"Cheung, S.C., Kramer, J.: Compositional reachability analysis of finite-state distributed systems with user-specified constraints. In: Proceedings of the 3rd ACM SIGSOFT International Symposium on the Foundations of Software Engineering (Washington, DC, USA), pp. 140\u2013150. ACM Press, Oct 1995","DOI":"10.1145\/222124.222149"},{"issue":"4","key":"244_CR19","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1145\/235321.235323","volume":"5","author":"S.C. Cheung","year":"1996","unstructured":"Cheung S.C., Kramer J.: Context constraints for compositional reachability. ACM Trans. Softw. Eng. Methodol. 5(4), 334\u2013377 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"244_CR20","unstructured":"Chossart, R.: \u00c9valuation d\u2019outils de v\u00e9rification pour les sp\u00e9cifications de syst\u00e8mes d\u2019information. M\u00e9moire ma\u00eetre \u00e8s sciences, Universit\u00e9 de Sherbrooke, Canada, Mar 2010"},{"key":"244_CR21","doi-asserted-by":"crossref","unstructured":"Clarke, E., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic. In: 10th Annual Symposium on Principles of Programming Languages. ACM, New York (1983)","DOI":"10.1145\/567067.567080"},{"issue":"2","key":"244_CR22","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke E.M., Emerson E.A., Sistla A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"244_CR23","unstructured":"Cleaveland, R., Li, T., Sims, S.: The Concurrency Workbench of the New Century (Version 1.2). User\u2019s manual, July 2000"},{"key":"244_CR24","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: The Concurrency Workbench. In: Proceedings of the 1st Workshop on Automatic Verification Methods for Finite State Systems (Grenoble, France). Lecture Notes in Computer Science, vol. 407, pp. 24\u201337. Springer, Berlin, June 1989","DOI":"10.1007\/3-540-52148-8_3"},{"key":"244_CR25","doi-asserted-by":"crossref","unstructured":"Cornejo, M.A., Garavel, H., Mateescu, R., de Palma, N.: Specification and verification of a dynamic reconfiguration protocol for agent-based applications. In: Proceedings of the 3rd IFIP WG 6.1 International Working Conference on Distributed Applications and Interoperable Systems DAIS\u20192001 (Krakow, Poland), pp. 229\u2013242. IFIP, Kluwer, Dordrecht, Sept 2001. Full version available as INRIA Research Report RR-4222","DOI":"10.1007\/0-306-47005-5_20"},{"key":"244_CR26","doi-asserted-by":"crossref","unstructured":"Coste, N., Garavel, H., Hermanns, H., Lang, F., Mateescu, R., Serwe, W.: Ten years of performance evaluation for concurrent systems using CADP. In: Proceedings of the 4th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation ISoLA 2010 (Amirandes, Heraclion, Crete), Part II. Lecture Notes in Computer Science, vol. 6416, pp. 128\u2013142. Springer, Berlin, Oct 2010","DOI":"10.1007\/978-3-642-16561-0_18"},{"key":"244_CR27","doi-asserted-by":"crossref","unstructured":"Coste, N., Hermanns, H., Lantreibecq, E., Serwe, W.: Towards performance prediction of compositional models in industrial GALS designs. In: Proceedings of the 21th International Conference on Computer Aided Verification CAV\u20192009 (Grenoble, France). Lecture Notes in Computer Science, vol. 5643, pp. 204\u2013218. Springer, Berlin, July 2009","DOI":"10.1007\/978-3-642-02658-4_18"},{"key":"244_CR28","doi-asserted-by":"crossref","unstructured":"Crouzen, P., Lang, F.: Smart reduction. In: Proceedings of Fundamental Approaches to Software Engineering FASE\u20192011 (Saarbr\u00fccken, Germany). Lecture Notes in Computer Science, vol. 6603, pp. 111\u2013126. Springer, Berlin, Mar 2011","DOI":"10.1007\/978-3-642-19811-3_9"},{"key":"244_CR29","doi-asserted-by":"crossref","unstructured":"Deavours, D.D., Sanders, W.H.: An efficient well-specified check. In: Proceedings of the 8th International Workshop on Petri Nets and Performance Models PNPM\u201999 (Zaragoza, Spain), pp. 124\u2013133. IEEE Press (1999)","DOI":"10.1109\/PNPM.1999.796559"},{"key":"244_CR30","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering ICSE\u201999 (Los Angeles, CA, USA), May 1999","DOI":"10.1145\/302405.302672"},{"key":"244_CR31","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional Mu-calculus. In: Proceedings of the 1st International Symposium on Logic in Computer Science LICS\u201986, pp. 267\u2013278 (1986)"},{"key":"244_CR32","unstructured":"Fernandez, J.-C.: ALDEBARAN: un syst\u00e8me de v\u00e9rification par r\u00e9duction de processus communicants. Th\u00e8se de Doctorat, Universit\u00e9 Joseph Fourier (Grenoble), May 1988"},{"key":"244_CR33","doi-asserted-by":"crossref","unstructured":"Fernandez, J.-C., Garavel, H., Kerbrat, A., Mateescu, R., Mounier, L., Sighireanu, M.: CADP (C\u00c6SAR\/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox. In: Proceedings of the 8th Conference on Computer-Aided Verification (New Brunswick, New Jersey, USA). Lecture Notes in Computer Science, vol. 1102, pp. 437\u2013440. Springer, Berlin, Aug 1996","DOI":"10.1007\/3-540-61474-5_97"},{"key":"244_CR34","doi-asserted-by":"crossref","unstructured":"Fernandez, J.-C., Garavel, H., Mounier, L., Rasse, A., Rodr\u00edguez, C., Sifakis, J.: A toolbox for the verification of LOTOS programs. In: Proceedings of the 14th International Conference on Software Engineering ICSE\u201914 (Melbourne, Australia), pp. 246\u2013259. ACM, New York, May 1992","DOI":"10.1145\/143062.143124"},{"key":"244_CR35","doi-asserted-by":"crossref","unstructured":"Fernandez, J.-C., Mounier, L.: \u201cOn the Fly\u201d verification of behavioural equivalences and preorders. In: Proceedings of the 3rd Workshop on Computer-Aided Verification (Aalborg, Denmark). Lecture Notes in Computer Science, vol. 575, pp. 181\u2013191. Springer, Berlin, July 1991","DOI":"10.1007\/3-540-55179-4_18"},{"key":"244_CR36","unstructured":"Fernandez, J.-C., Richier, J.-L., Voiron, J.: Verification of protocol specifications using the CESAR system. In: Proceedings of the 5th IFIP International Workshop on Protocol Specification, Testing and Verification (Moissac, France), pp. 71\u201390. IFIP, North-Holland, June 1985"},{"issue":"2","key":"244_CR37","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"Fischer M.J., Ladner R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"244_CR38","unstructured":"Garavel, H.: Compilation et v\u00e9rification de programmes LOTOS. Th\u00e8se de Doctorat, Universit\u00e9 Joseph Fourier (Grenoble), Nov 1989"},{"key":"244_CR39","unstructured":"Garavel, H.: Compilation of LOTOS abstract data types. In: Proceedings of the 2nd International Conference on Formal Description Techniques FORTE\u201989 (Vancouver B.C., Canada), pp. 147\u2013162. North-Holland, Dec 1989"},{"key":"244_CR40","unstructured":"Garavel, H.: On the introduction of gate typing in E-LOTOS. Rapport SPECTRE 94-3, VERIMAG, Grenoble, Feb. 1994. Annex D of ISO\/IEC JTC1\/SC21\/WG1 N1314 Revised Draft on Enhancements to LOTOS and Annex C of ISO\/IEC JTC1\/SC21\/WG1 N1349 Working Draft on Enhancements to LOTOS"},{"key":"244_CR41","doi-asserted-by":"crossref","unstructured":"Garavel, H.: OPEN\/C\u00c6SAR: an open software architecture for verification, simulation, and testing. In: Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS\u201998 (Lisbon, Portugal). Lecture Notes in Computer Science, vol. 1384, pp. 68\u201384, Springer, Berlin, Mar 1998. Full version available as INRIA Research Report RR-3352","DOI":"10.1007\/BFb0054165"},{"key":"244_CR42","unstructured":"Garavel, H.: D\u00e9fense et illustration des alg\u00e8bres de processus. In Actes de l\u2019Ecole d\u2019\u00e9t\u00e9 Temps R\u00e9el ETR 2003 (Toulouse, France). Institut de Recherche en Informatique de Toulouse, Sept 2003"},{"key":"244_CR43","doi-asserted-by":"crossref","unstructured":"Garavel, H.: Reflections on the future of concurrency theory in general and process calculi in particular. In: Proceedings of the LIX Colloquium on Emerging Trends in Concurrency Theory (Ecole Polytechnique de Paris, France), November 13\u201315, 2006. Electronic Notes in Theoretical Computer Science, vol. 209, pp. 149\u2013164. Elsevier, Amsterdam, Apr 2008. Also available as INRIA Research Report RR-6368","DOI":"10.1016\/j.entcs.2008.04.009"},{"key":"244_CR44","doi-asserted-by":"crossref","unstructured":"Garavel, H., Helmstetter, C., Ponsini, O., Serwe, W.: Verification of an industrial SystemC\/TLM model using LOTOS and CADP. In: Proceedings of the 7th ACM-IEEE International Conference on Formal Methods and Models for Codesign MEMOCODE\u20192009 (Cambridge, MA, USA). IEEE Computer Society Press, June 2009","DOI":"10.1109\/MEMCOD.2009.5185377"},{"key":"244_CR45","doi-asserted-by":"crossref","unstructured":"Garavel, H., Hermanns, H.: On combining functional verification and performance evaluation using CADP. In: Proceedings of the 11th International Symposium of Formal Methods Europe FME\u20192002 (Copenhagen, Denmark). Lecture Notes in Computer Science, vol. 2391, pp. 410\u2013429. Springer, Berlin, July 2002. Full version available as INRIA Research Report 4492","DOI":"10.1007\/3-540-45614-7_23"},{"key":"244_CR46","doi-asserted-by":"crossref","unstructured":"Garavel, H., Lang, F.: SVL: a scripting language for compositional verification. In: Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE\u20192001 (Cheju Island, Korea), pp. 377\u2013392. IFIP, Kluwer, Dordrecht, Aug 2001. Full version available as INRIA Research Report RR-4223","DOI":"10.1007\/0-306-47003-9_24"},{"key":"244_CR47","unstructured":"Garavel, H., Lang, F., Mateescu, R.: An overview of CADP 2001. Eur. Assoc. Softw. Sci. Technol. Newsl. 4, 13\u201324 (2002). Also available as INRIA Technical Report RT-0254, Dec 2001"},{"key":"244_CR48","doi-asserted-by":"crossref","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Proceedings of the 19th International Conference on Computer Aided Verification CAV\u20192007 (Berlin, Germany). Lecture Notes in Computer Science, vol. 4590, pp. 158\u2013163. Springer, Berlin, July 2007","DOI":"10.1007\/978-3-540-73368-3_18"},{"key":"244_CR49","doi-asserted-by":"crossref","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: a toolbox for the construction and analysis of distributed processes. In: Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS\u20192011 (Saarbr\u00fccken, Germany). Lecture Notes in Computer Science, vol. 6605, pp. 372\u2013387. Springer, Berlin, Mar 2011","DOI":"10.1007\/978-3-642-19835-9_33"},{"key":"244_CR50","unstructured":"Garavel, H., Mateescu, R.: SEQ.OPEN: a tool for efficient trace-based verification. In: Proceedings of the 11th International SPIN Workshop on Model Checking of Software SPIN\u20192004 (Barcelona, Spain). Lecture Notes in Computer Science, vol. 2989, pp. 150\u2013155. Springer, Berlin, Apr 2004"},{"key":"244_CR51","doi-asserted-by":"crossref","unstructured":"Garavel, H., Mateescu, R., Bergamini, D., Curic, A., Descoubes, N., Joubert, C., Smarandache-Sturm, I., Stragier, G.: DISTRIBUTOR and BCG_MERGE: tools for distributed explicit state space generation. In: Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS\u20192006 (Vienna, Austria). Lecture Notes in Computer Science, vol. 3920, pp. 445\u2013449. Springer, Berlin, Mar\u2013Apr 2006","DOI":"10.1007\/11691372_30"},{"key":"244_CR52","doi-asserted-by":"crossref","unstructured":"Garavel, H., Mateescu, R., Smarandache, I.: Parallel state space construction for model-checking. In: Proceedings of the 8th International SPIN Workshop on Model Checking of Software SPIN\u20192001 (Toronto, Canada). Lecture Notes in Computer Science, vol. 2057, pp. 217\u2013234. Springer, Berlin, May 2001. Revised version available as INRIA Research Report RR-4341, Dec 2001","DOI":"10.1007\/3-540-45139-0_14"},{"issue":"3","key":"244_CR53","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1016\/j.scico.2008.09.011","volume":"74","author":"H. Garavel","year":"2009","unstructured":"Garavel H., Sala\u00fcn G., Serwe W.: On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP. Sci. Comput. Program. 74(3), 100\u2013127 (2009)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"244_CR54","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/j.tcs.2005.09.064","volume":"351","author":"H. Garavel","year":"2006","unstructured":"Garavel H., Serwe W.: State space reduction for process algebra specifications. Theor. Comput. Sci. 351(2), 131\u2013145 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"244_CR55","unstructured":"Garavel, H., Sifakis, J.: Compilation and verification of LOTOS specifications. In: Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification (Ottawa, Canada), pp. 379\u2013394. IFIP, North-Holland, June 1990"},{"key":"244_CR56","unstructured":"Garavel, H., Sighireanu, M.: Towards a second generation of formal description techniques\u2014rationale for the design of E-LOTOS. In: Proceedings of the 3rd International Workshop on Formal Methods for Industrial Critical Systems FMICS\u201998 (Amsterdam, The Netherlands), pp. 187\u2013230, Amsterdam, May 1998. CWI. Invited lecture"},{"key":"244_CR57","doi-asserted-by":"crossref","unstructured":"Garavel, H., Sighireanu, M.: A graphical parallel composition operator for process algebras. In: Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification FORTE\/PSTV\u201999 (Beijing, China), pp. 185\u2013202. IFIP, Kluwer, Dordrecht, Oct 1999","DOI":"10.1007\/978-0-387-35578-8_11"},{"key":"244_CR58","doi-asserted-by":"crossref","unstructured":"Garavel, H., Thivolle, D.: Verification of GALS systems by combining synchronous languages and process calculi. In: Model Checking Software, Proceedings of the 16th International SPIN Workshop on Model Checking of Software SPIN\u20192009 (Grenoble, France). Lecture Notes in Computer Science, vol. 5578, pp. 241\u2013260. Springer, Berlin, June 2009","DOI":"10.1007\/978-3-642-02652-2_20"},{"key":"244_CR59","unstructured":"Garavel, H., Turlier, P.: C\u00c6SAR.ADT: un compilateur pour les types abstraits alg\u00e9briques du langage LOTOS. In: Actes du Colloque Francophone pour l\u2019Ing\u00e9nierie des Protocoles CFIP\u201993 (Montr\u00e9al, Canada) (1993)"},{"key":"244_CR60","unstructured":"Garavel, H., Viho, C., Zendri, M.: System design of a CC-NUMA multiprocessor architecture using formal specification, model-checking, co-simulation, and test generation. Springer Int. J. Softw. Tools Technol. Transfer 3(3), 314\u2013331 (2001). Also available as INRIA Research Report RR-4041"},{"key":"244_CR61","unstructured":"Giannakopoulou, D.: Model checking for concurrent software architectures. PhD thesis, Imperial College of Science, Technology and Medicine\u2014University of London\u2014Department of Computer Science, Jan 1999"},{"key":"244_CR62","doi-asserted-by":"crossref","unstructured":"Graf, S., Richier, J.-L., Rodr\u00edguez, C., Voiron, J.: What are the limits of model checking methods for the verification of real life protocols? In: Proceedings of the 1st Workshop on Automatic Verification Methods for Finite State Systems (Grenoble, France). Lecture Notes in Computer Science, vol. 407, pp. 275\u2013285. Springer, Berlin, June 1989","DOI":"10.1007\/3-540-52148-8_23"},{"key":"244_CR63","doi-asserted-by":"crossref","unstructured":"Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Proceedings of the 2nd Workshop on Computer-Aided Verification (Rutgers, New Jersey, USA). Lecture Notes in Computer Science, vol. 531, pp. 186\u2013196. Springer, Berlin, June 1990","DOI":"10.1007\/BFb0023732"},{"issue":"5","key":"244_CR64","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1007\/BF01211911","volume":"8","author":"S. Graf","year":"1996","unstructured":"Graf S., Steffen B., L\u00fcttgen G.: Compositional minimisation of finite state systems using interface specifications. Formal Asp. Comput. 8(5), 607\u2013616 (1996)","journal-title":"Formal Asp. Comput."},{"key":"244_CR65","doi-asserted-by":"crossref","unstructured":"Groote, J., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Proceedings of the 17th ICALP (Warwick). Lecture Notes in Computer Science, vol. 443, pp. 626\u2013638. Springer, Berlin (1990)","DOI":"10.1007\/BFb0032063"},{"key":"244_CR66","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Ponse, A.: The syntax and semantics of\u00a0\u03bcCRL. In: Algebra of Communicating Processes\u201994, Workshops in Computing Series, pp. 26\u201362. Springer, Berlin (1995)","DOI":"10.1007\/978-1-4471-2120-6_2"},{"key":"244_CR67","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1016\/j.tcs.2005.06.016","volume":"343","author":"J.F. Groote","year":"2005","unstructured":"Groote J.F., Willemse T.A.C.: Parameterised Boolean equation systems. Theor. Comput. Sci. 343, 332\u2013369 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"244_CR68","unstructured":"Helmstetter, C.: TLM.OPEN: a SystemC\/TLM Front-End for the CADP Verification Toolbox. Workshop on Simulation Based Development of Certified Embedded Systems SBDCES\u201909 (Awaji Island, Hyogo, Japan), Oct 2009"},{"key":"244_CR69","doi-asserted-by":"crossref","unstructured":"Helmstetter, C., Ponsini, O.: A comparison of two SystemC\/TLM semantics for formal verification. In: Proceedings of the 6th ACM-IEEE International Conference on Formal Methods and Models for Codesign MEMOCODE\u20192008 (Anaheim, CA, USA), pp. 59\u201368. IEEE Computer Society Press, June 2008","DOI":"10.1109\/MEMCOD.2008.4547687"},{"key":"244_CR70","volume-title":"Interactive Markov Chains and the Quest for Quantified Quality. Lecture Notes in Computer Science, vol. 2428","author":"H. Hermanns","year":"2002","unstructured":"Hermanns H.: Interactive Markov Chains and the Quest for Quantified Quality. Lecture Notes in Computer Science, vol. 2428. Springer, Berlin (2002)"},{"key":"244_CR71","doi-asserted-by":"crossref","unstructured":"Hermanns, H., Joubert, C.: A set of performance and dependability analysis components for CADP. In: Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS\u20192003 (Warsaw, Poland). Lecture Notes in Computer Science, vol. 2619, pp. 425\u2013430. Springer, Berlin, April 2003","DOI":"10.1007\/3-540-36577-X_30"},{"key":"244_CR72","doi-asserted-by":"crossref","unstructured":"Hermanns, H., Siegle, M.: Bisimulation algorithms for stochastic process algebras and their BDD-based implementation. In: Proceedings of the 5th International AMAST Workshop ARTS\u201999 (Bamberg, Germany). Lecture Notes in Computer Science, vol. 1601, pp. 244\u2013265. Springer, Berlin, May 1999","DOI":"10.1007\/3-540-48778-6_15"},{"issue":"8","key":"244_CR73","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"Hoare C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"244_CR74","volume-title":"Design and Validation of Computer Protocols. Software Series","author":"G.J. Holzmann","year":"1991","unstructured":"Holzmann G.J.: Design and Validation of Computer Protocols. Software Series. Prentice Hall, Englewood Cliffs (1991)"},{"key":"244_CR75","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"244_CR76","unstructured":"ISO\/IEC.: LOTOS\u2014a formal description technique based on the temporal ordering of observational behaviour. International Standard 8807, International Organization for Standardization\u2014Information Processing Systems\u2014Open Systems Interconnection, Gen\u00e8ve, Sept 1989"},{"key":"244_CR77","unstructured":"ISO\/IEC. Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization\u2014Information Technology, Gen\u00e8ve, Sept 2001"},{"key":"244_CR78","unstructured":"ITU-T.: Specification and Description Language (SDL). ITU-T Recommendation Z.100. International Telecommunication Union, Gen\u00e8ve (1992)"},{"issue":"1","key":"244_CR79","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P.C. Kanellakis","year":"1990","unstructured":"Kanellakis P.C., Smolka S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43\u201368 (1990)","journal-title":"Inf. Comput."},{"key":"244_CR80","volume-title":"Finite Markov Chains","author":"J.G. Kemeny","year":"1976","unstructured":"Kemeny J.G., Snell J.L.: Finite Markov Chains. Springer, Berlin (1976)"},{"key":"244_CR81","unstructured":"Khan, A.M.: Connection of Compositional Verification Tools for Embedded Systems. M\u00e9moire master 2 recherche, Universit\u00e9 Joseph Fourier, Grenoble, June 2006"},{"key":"244_CR82","doi-asserted-by":"crossref","unstructured":"Krimm, J.-P., Mounier, L.: Compositional State Space Generation from LOTOS Programs. In: Proceedings of TACAS\u201997 Tools and Algorithms for the Construction and Analysis of Systems (University of Twente, Enschede, The Netherlands). Lecture Notes in Computer Science, vol. 1217. Springer, Berlin, April 1997","DOI":"10.1007\/BFb0035392"},{"key":"244_CR83","doi-asserted-by":"crossref","unstructured":"Lang, F.: Compositional verification using SVL scripts. In: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS\u20192002 (Grenoble, France). Lecture Notes in Computer Science, vol. 2280, pp. 465\u2013469. Springer, Berlin, April 2002","DOI":"10.1007\/3-540-46002-0_33"},{"key":"244_CR84","doi-asserted-by":"crossref","unstructured":"Lang, F.: EXP.OPEN 2.0: a flexible tool integrating partial order, compositional, and on-the-fly verification methods. In: Proceedings of the 5th International Conference on Integrated Formal Methods IFM\u20192005 (Eindhoven, The Netherlands). Lecture Notes in Computer Science, vol. 3771, pp. 70\u201388. Springer, Berlin, Nov 2005. Full version available as INRIA Research Report RR-5673","DOI":"10.1007\/11589976_6"},{"issue":"6","key":"244_CR85","doi-asserted-by":"crossref","first-page":"681","DOI":"10.1007\/s00165-009-0133-8","volume":"22","author":"F. Lang","year":"2010","unstructured":"Lang F., Sala\u00fcn G., H\u00e9rilier R., Kramer J., Magee J.: Translating FSP into LOTOS and Networks of Automata. Formal Asp. Comput. 22(6), 681\u2013711 (2010)","journal-title":"Formal Asp. Comput."},{"key":"244_CR86","doi-asserted-by":"crossref","unstructured":"Lantreibecq, E., Serwe, W.: Model checking and co-simulation of a dynamic task dispatcher circuit using CADP. In: Proceedings of the 16th International Workshop on Formal Methods for Industrial Critical Systems FMICS 2011 (Trento, Italy). Lecture Notes in Computer Science, vol. 6959, pp. 180\u2013195. Springer, Berlin, Aug 2011","DOI":"10.1007\/978-3-642-24431-5_14"},{"key":"244_CR87","doi-asserted-by":"crossref","unstructured":"Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points. In: Proceedings of the 25th International Colloquium on Automata, Languages, and Programming ICALP\u201998 (Aalborg, Denmark). Lecture Notes in Computer Science, vol. 1443, pp. 53\u201366. Springer, Berlin, July 1998","DOI":"10.1007\/BFb0055040"},{"key":"244_CR88","doi-asserted-by":"crossref","unstructured":"Liu, Y., Sun, J., Dong, J.S.: Developing model checkers using PAT. In: Proceedings of the 8th International Symposium on Automated Technology for Verification and Analysis ATVA 2010 (Singapore). Lecture Notes in Computer Science, vol. 6252, pp. 371\u2013377. Springer, Berlin, Sept 2010","DOI":"10.1007\/978-3-642-15643-4_30"},{"key":"244_CR89","volume-title":"Verification of Modal Properties Using Boolean Equation Systems. VERSAL 8","author":"A. Mader","year":"1997","unstructured":"Mader A.: Verification of Modal Properties Using Boolean Equation Systems. VERSAL 8. Bertz Verlag, Berlin (1997)"},{"key":"244_CR90","unstructured":"Magee, J., Kramer, J.: Concurrency: State Models and Java Programs. Wiley, New York (2006)"},{"key":"244_CR91","doi-asserted-by":"crossref","unstructured":"Malhotra, J., Smolka, S.A., Giacalone, A., Shapiro, R.: A tool for hierarchical design and simulation of concurrent systems. In: Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems (Stirling, Scotland), pp. 140\u2013152, Swindon, UK. British Computer Society, July 1988","DOI":"10.1007\/978-1-4471-3534-0_7"},{"key":"244_CR92","unstructured":"Mateescu, R.: V\u00e9rification des propri\u00e9t\u00e9s temporelles des programmes parall\u00e8les. Th\u00e8se de Doctorat, Institut National Polytechnique de Grenoble, April 1998"},{"key":"244_CR93","doi-asserted-by":"crossref","unstructured":"Mateescu, R.: Efficient diagnostic generation for Boolean equation systems. In: Proceedings of 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS\u20192000 (Berlin, Germany). Lecture Notes in Computer Science, vol. 1785, pp. 251\u2013265. Springer, Berlin, Mar 2000. Full version available as INRIA Research Report RR-3861","DOI":"10.1007\/3-540-46419-0_18"},{"key":"244_CR94","doi-asserted-by":"crossref","unstructured":"Mateescu, R.: A generic on-the-fly solver for alternation-free Boolean equation systems. In: Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS\u20192003 (Warsaw, Poland). Lecture Notes in Computer Science, vol. 2619, pp. 81\u201396. Springer, Berlin, April 2003. Full version available as INRIA Research Report RR-4711","DOI":"10.1007\/3-540-36577-X_7"},{"key":"244_CR95","doi-asserted-by":"crossref","unstructured":"Mateescu, R.: CAESAR_SOLVE: a generic library for on-the-fly resolution of alternation-free Boolean equation systems. Springer Int. J. Softw. Tools Technol. Transfer 8(1), 37\u201356 (2006). Full version available as INRIA Research Report RR-5948, July 2006","DOI":"10.1007\/s10009-005-0194-9"},{"key":"244_CR96","unstructured":"Mateescu, R., Garavel, H.: XTL: a meta-language and tool for temporal logic model-checking. In: Proceedings of the International Workshop on Software Tools for Technology Transfer STTT\u201998 (Aalborg, Denmark), pp. 33\u201342. BRICS, July 1998"},{"key":"244_CR97","doi-asserted-by":"crossref","unstructured":"Mateescu, R., Oudot, E.: Improved on-the-fly equivalence checking using Boolean equation systems. In: Proceedings of the 15th International SPIN Workshop on Model Checking of Software SPIN\u20192008 (Los Angeles, USA). Lecture Notes in Computer Science, vol. 5156, pp. 196\u2013213. Springer, Berlin, Aug 2008. Full version available as INRIA Research Report RR-6777","DOI":"10.1007\/978-3-540-85114-1_15"},{"key":"244_CR98","doi-asserted-by":"crossref","unstructured":"Mateescu, R., Sala\u00fcn, G.: Translating Pi-Calculus into LOTOS NT. In: Proceedings of the 8th International Conference on Integrated Formal Methods IFM\u20192010 (Nancy, France). Lecture Notes in Computer Science, vol. 6396, pp. 229\u2013244. Springer, Berlin, Oct 2010","DOI":"10.1007\/978-3-642-16265-7_17"},{"key":"244_CR99","doi-asserted-by":"crossref","unstructured":"Mateescu, R., Serwe, W.: Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols. Sci. Comput. Program. (2012). doi: 10.1016\/j.scico.2012.01.003","DOI":"10.1016\/j.scico.2012.01.003"},{"issue":"3","key":"244_CR100","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/S0167-6423(02)00094-1","volume":"46","author":"R. Mateescu","year":"2003","unstructured":"Mateescu R., Sighireanu M.: Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. Sci. Comput. Program. 46(3), 255\u2013281 (2003)","journal-title":"Sci. Comput. Program."},{"key":"244_CR101","doi-asserted-by":"crossref","unstructured":"Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Proceedings of the 15th International Symposium on Formal Methods FM\u201908 (Turku, Finland). Lecture Notes in Computer Science, vol. 5014, pp. 148\u2013164. Springer, Berlin, May 2008","DOI":"10.1007\/978-3-540-68237-0_12"},{"issue":"1","key":"244_CR102","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/103727.103729","volume":"9","author":"J.M. Mellor-Crummey","year":"1991","unstructured":"Mellor-Crummey J.M., Scott M.L.: Algorithms for scalable synchronization on shared-memory multiprocessors. ACM Trans. Comput. Syst. 9(1), 21\u201365 (1991)","journal-title":"ACM Trans. Comput. Syst."},{"key":"244_CR103","unstructured":"Milne, G.J.: CIRCAL and the representation of communication, concurrency, and time. ACM Trans. Program. Lang. Syst. 7(2), 270\u2013298 (1985)"},{"key":"244_CR104","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"244_CR105","doi-asserted-by":"crossref","unstructured":"Nicola, R.D., Vaandrager, F.W.: Action versus State Based Logics for Transition Systems. Lecture Notes in Computer Science, vol. 469, pp. 407\u2013419. Springer, Berlin (1990)","DOI":"10.1007\/3-540-53479-2_17"},{"key":"244_CR106","doi-asserted-by":"crossref","unstructured":"Pecheur, C.: Specification and verification of the CO4 distributed knowledge system using LOTOS. In: Proceedings of the 12th IEEE International Conference on Automated Software Engineering ASE-97 (Incline Village, Nevada, USA), Nov 1997","DOI":"10.1109\/ASE.1997.632825"},{"key":"244_CR107","unstructured":"Pecheur, C.: Advanced modelling and verification techniques applied to a cluster file system. In: Proceedings of the 14th IEEE International Conference on Automated Software Engineering ASE-99 (Cocoa Beach, Florida, USA). IEEE Computer Society, Oct 1999"},{"issue":"3","key":"244_CR108","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1016\/j.scico.2004.10.001","volume":"56","author":"O. Ponsini","year":"2005","unstructured":"Ponsini O., F\u00e9d\u00e8le C., Kounalis E.: Rewriting of imperative programs into logical equations. Sci. Comput. Program. 56(3), 363\u2013401 (2005)","journal-title":"Sci. Comput. Program."},{"key":"244_CR109","doi-asserted-by":"crossref","unstructured":"Ponsini, O., Serwe, W.: A Schedulerless semantics of TLM models written in SystemC via translation into LOTOS. In: Proceedings of the 15th International Symposium on Formal Methods FM\u201908 (Turku, Finland). Lecture Notes in Computer Science, vol. 5014, pp. 278\u2013293. Springer, Berlin, May 2008","DOI":"10.1007\/978-3-540-68237-0_20"},{"key":"244_CR110","volume-title":"Le syst\u00e8me CESAR: description, sp\u00e9cification et analyse des applications r\u00e9parties","author":"J.-P. Queille","year":"1982","unstructured":"Queille J.-P.: Le syst\u00e8me CESAR: description, sp\u00e9cification et analyse des applications r\u00e9parties. Universit\u00e9 Scientifique et M\u00e9dicale de Grenoble, Grenoble (1982)"},{"key":"244_CR111","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1998","unstructured":"Roscoe A.W.: The Theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs (1998)"},{"key":"244_CR112","unstructured":"Rose, A., Swan, S., Pierce, J., Fernandez, J.-M.: Transaction Level Modeling in SystemC. Open SystemC Initiative (2005)"},{"issue":"9","key":"244_CR113","doi-asserted-by":"crossref","first-page":"940","DOI":"10.1109\/26.35374","volume":"37","author":"K.K. Sabnani","year":"1989","unstructured":"Sabnani K.K., Lapone A.M., Uyar M.U.: An algorithmic procedure for checking safety properties of protocols. IEEE Trans. Commun. 37(9), 940\u2013948 (1989)","journal-title":"IEEE Trans. Commun."},{"key":"244_CR114","doi-asserted-by":"crossref","unstructured":"Sala\u00fcn, G., Etchevers, X., Palma, N.D., Boyer, F., Coupaye, T.: Verification of a self-configuration protocol for distributed applications in the cloud. In: Proceedings of the 27th Symposium On Applied Computing SAC\u201912 (Riva del Garda, Italy). ACM, New York (2012, to appear)","DOI":"10.1145\/2245276.2231979"},{"key":"244_CR115","doi-asserted-by":"crossref","unstructured":"Schewe, S.: Solving Parity games in big steps. In: Proceedings of the 27th International Conference on Software Technology and Theoretical Computer Science FSTTCS\u201907 (New Delhi, India). Lecture Notes in Computer Science, vol. 4855, pp. 449\u2013460. Springer, Berlin, Dec 2007","DOI":"10.1007\/978-3-540-77050-3_37"},{"key":"244_CR116","doi-asserted-by":"crossref","unstructured":"Stevens, P., Stirling, C.: Practical model-checking using games. In: Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS\u201998 (Lisbon, Portugal). Lecture Notes in Computer Science, vol. 1384, pp. 85\u2013101. Springer, Berlin, Mar 1998","DOI":"10.1007\/BFb0054166"},{"key":"244_CR117","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"R. Streett","year":"1982","unstructured":"Streett R.: Propositional dynamic logic of looping and converse. Inf. Control 54, 121\u2013141 (1982)","journal-title":"Inf. Control"},{"key":"244_CR118","doi-asserted-by":"crossref","unstructured":"Tai, K.C., Koppol, V.: Hierarchy-based incremental reachability analysis of communication protocols. In: Proceedings of the IEEE International Conference on Network Protocols (San Francisco, CA), pp. 318\u2013325. IEEE Press, Piscataway, Oct 1993","DOI":"10.1109\/ICNP.1993.340896"},{"key":"244_CR119","unstructured":"Tai, K.C., Koppol, V.: An incremental approach to reachability analysis of distributed programs. In: Proceedings of the 7th International Workshop on Software Specification and Design (Los Angeles, CA), pp. 141\u2013150. IEEE Press, Piscataway, Dec 1993"},{"key":"244_CR120","unstructured":"Thivolle, D.: Langages modernes pour la v\u00e9rification des syst\u00e8mes asynchrones. Th\u00e8se de Doctorat, Universit\u00e9 Joseph Fourier (Grenoble, France) and Universitatea Politehnica din Bucuresti (Bucharest, Romania), April 2011"},{"key":"244_CR121","doi-asserted-by":"crossref","unstructured":"Tronel, F., Lang, F., Garavel, H.: Compositional verification using CADP of the ScalAgent deployment protocol for software components. In: Proceedings of the 6th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems FMOODS\u20192003 (Paris, France). Lecture Notes in Computer Science, vol. 2884, pp. 244\u2013260. Springer, Berlin, Nov 2003. Full version available as INRIA Research Report RR-5012","DOI":"10.1007\/978-3-540-39958-2_17"},{"key":"244_CR122","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Compositional state space generation. In: Proceedings of Advances in Petri Nets. Lecture Notes in Computer Science, vol. 674, pp. 427\u2013457. Springer, Berlin (1993)","DOI":"10.1007\/3-540-56689-9_54"},{"key":"244_CR123","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching-time and abstraction in bisimulation semantics (extended abstract). CS R8911, Centrum voor Wiskunde en Informatica, Amsterdam, 1989. Also in Proc. IFIP 11th World Computer Congress, San Francisco (1989)"},{"key":"244_CR124","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1147\/rd.224.0393","volume":"22","author":"C. West","year":"1978","unstructured":"West C.: A general technique for communication protocol validation. IBM J. Res. Dev. 22, 393\u2013404 (1978)","journal-title":"IBM J. Res. Dev."},{"key":"244_CR125","unstructured":"Wolper, P.: A translation from full branching time temporal logic to one letter propositional dynamic logic with looping. Unpublished manuscript (1982)"},{"key":"244_CR126","unstructured":"Yeh, W.J.: Controlling state explosion in reachability analysis. PhD thesis, Software Engineering Research Center (SERC) Laboratory, Purdue University. Technical Report SERC-TR-147-P, Dec 1993"},{"key":"244_CR127","doi-asserted-by":"crossref","unstructured":"Yeh, W.J., Young, M.: Compositional reachability analysis using process algebra. In: Proceedings of the ACM SIGSOFT Symposium on Testing, Analysis, and Verification (SIGSOFT\u201991, Victoria, British Columbia, Canada), pp. 49\u201359. ACM Press, New York, Oct 1991","DOI":"10.1145\/120807.120812"},{"issue":"1\/2","key":"244_CR128","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine S.: Kronos: a verification tool for real-time systems. Springer Int. J. Softw. Tools Technol. Transfer 1(1\/2), 123\u2013133 (1997)","journal-title":"Springer Int. J. Softw. Tools Technol. Transfer"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0244-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0244-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0244-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T16:22:20Z","timestamp":1743697340000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0244-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,30]]},"references-count":128,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,4]]}},"alternative-id":["244"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0244-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6,30]]}}}