{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T14:46:21Z","timestamp":1791125181852,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642385919","type":"print"},{"value":"9783642385926","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38592-6_11","type":"book-chapter","created":{"date-parts":[[2013,5,29]],"date-time":"2013-05-29T04:56:11Z","timestamp":1369803371000},"page":"146-160","source":"Crossref","is-referenced-by-count":9,"title":["Formal Verification of Distributed Branching Multiway Synchronization Protocols"],"prefix":"10.1007","author":[{"given":"Hugues","family":"Evrard","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Lang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"9","key":"11_CR1","doi-asserted-by":"publisher","first-page":"1053","DOI":"10.1109\/32.31364","volume":"15","author":"R. Bagrodia","year":"1989","unstructured":"Bagrodia, R.: Process synchronization: Design and performance evaluation of distributed algorithms. IEEE Trans. on Software Engineering\u00a015(9), 1053\u20131065 (1989)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: From high-level component-based models to distributed implementations. In: Proc. of the 10th ACM International Conference on Embedded Software, pp. 209\u2013218 (2010)","DOI":"10.1145\/1879021.1879049"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-54233-7_126","volume-title":"Automata, Languages and Programming","author":"A. Bouajjani","year":"1991","unstructured":"Bouajjani, A., Fernandez, J.C., Graf, S., Rodr\u00edguez, C., Sifakis, J.: Safety for Branching Time Semantics. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510, pp. 76\u201392. Springer, Heidelberg (1991)"},{"issue":"3","key":"11_CR4","doi-asserted-by":"publisher","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. Journal of the ACM\u00a031(3), 560\u2013599 (1984)","journal-title":"Journal of the ACM"},{"key":"11_CR5","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.8). Inria\/CONVECS (2013)"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley (1988)","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-16561-0_18","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"N. Coste","year":"2010","unstructured":"Coste, N., Garavel, H., Hermanns, H., Lang, F., Mateescu, R., Serwe, W.: Ten Years of Performance Evaluation for Concurrent Systems Using CADP. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part II. LNCS, vol.\u00a06416, pp. 128\u2013142. Springer, Heidelberg (2010)"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: The Structure of the \u201cTHE\u201d-Multiprogramming System. Comm. of the ACM (1968)","DOI":"10.1007\/978-1-4757-3472-0_3"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/BFb0054165","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Garavel","year":"1998","unstructured":"Garavel, H.: OPEN\/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 68\u201384. Springer, Heidelberg (1998)"},{"key":"11_CR10","unstructured":"Garavel, H., Lang, F.: SVL: a Scripting Language for Compositional Verification. In: Proc. of FORTE. Kluwer (2001)"},{"issue":"2","key":"11_CR11","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H. Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. STTT\u00a015(2), 89\u2013107 (2013)","journal-title":"STTT"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Garavel, H., Sighireanu, M.: A Graphical Parallel Composition Operator for Process Algebras. In: Proc. of FORTE\/PSTV. Kluwer (1999)","DOI":"10.1007\/978-0-387-35578-8_11"},{"issue":"3","key":"11_CR13","doi-asserted-by":"crossref","first-page":"314","DOI":"10.1007\/s100090100044","volume":"3","author":"H. Garavel","year":"2001","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. STTT\u00a03(3), 314\u2013331 (2001)","journal-title":"STTT"},{"issue":"2","key":"11_CR14","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1147\/sj.72.0074","volume":"7","author":"J.W. Havender","year":"1968","unstructured":"Havender, J.W.: Avoiding deadlock in multitasking systems. IBM Systems Journal\u00a07(2), 74\u201384 (1968)","journal-title":"IBM Systems Journal"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"11_CR16","unstructured":"ISO\/IEC. LOTOS \u2014 A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization (1989)"},{"key":"11_CR17","unstructured":"ISO\/IEC. Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization (2001)"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/11589976_6","volume-title":"Integrated Formal Methods","author":"F. Lang","year":"2005","unstructured":"Lang, F.: EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol.\u00a03771, pp. 70\u201388. Springer, Heidelberg (2005)"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Mateescu, R., Oudot, E.: Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems. In: Proc. of MEMOCODE. IEEE (2008)","DOI":"10.1109\/MEMCOD.2008.4547690"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-68237-0_12","volume-title":"FM 2008: Formal Methods","author":"R. Mateescu","year":"2008","unstructured":"Mateescu, R., Thivolle, D.: A Model Checking Language for Concurrent Value-Passing Systems. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 148\u2013164. Springer, Heidelberg (2008)"},{"key":"11_CR21","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall (1989)"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D. Park","year":"1981","unstructured":"Park, D.: Concurrency and Automata on Infinite Sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol.\u00a0104, pp. 167\u2013183. Springer, Heidelberg (1981)"},{"issue":"14","key":"11_CR23","doi-asserted-by":"publisher","first-page":"1151","DOI":"10.1016\/S0140-3664(96)01149-8","volume":"19","author":"J. Parrow","year":"1996","unstructured":"Parrow, J., Sj\u00f6din, P.: Designing a multiway synchronization protocol. Computer Communications\u00a019(14), 1151\u20131160 (1996)","journal-title":"Computer Communications"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/BFb0084813","volume-title":"CONCUR \u201992","author":"J. Parrow","year":"1992","unstructured":"Parrow, J., Sj\u00f6din, P.: Multiway synchronization verified with coupled simulation. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol.\u00a0630, pp. 518\u2013533. Springer, Heidelberg (1992)"},{"issue":"12","key":"11_CR25","doi-asserted-by":"publisher","first-page":"1173","DOI":"10.1002\/cpe.903","volume":"16","author":"J.A. P\u00e9rez","year":"2004","unstructured":"P\u00e9rez, J.A., Corchuelo, R., Toro, M.: An order-based algorithm for implementing multiparty synchronization. Concurrency and Computation: Practice and Experience\u00a016(12), 1173\u20131206 (2004)","journal-title":"Concurrency and Computation: Practice and Experience"},{"issue":"4","key":"11_CR26","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1109\/12.88463","volume":"40","author":"R. Sisto","year":"1991","unstructured":"Sisto, R., Ciminiera, L., Valenzano, A.: A protocol for multirendezvous of LOTOS processes. IEEE Trans. on Computers\u00a040(4), 437\u2013447 (1991)","journal-title":"IEEE Trans. on Computers"},{"key":"11_CR27","unstructured":"Sj\u00f6din, P.: From LOTOS Specifications to Distributed Implementations. PhD thesis, Department of Computer Science, University of Uppsala, Sweden (1991)"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-00255-7_7","volume-title":"Integrated Formal Methods","author":"J. St\u00f6cker","year":"2009","unstructured":"St\u00f6cker, J., Lang, F., Garavel, H.: Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol.\u00a05423, pp. 88\u2013102. Springer, Heidelberg (2009)"},{"key":"11_CR29","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching-Time and Abstraction in Bisimulation Semantics. In: Proc. of IFIP (1989)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38592-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,23]],"date-time":"2022-02-23T02:01:43Z","timestamp":1645581703000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38592-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385919","9783642385926"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38592-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}