{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:48:57Z","timestamp":1742921337279,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642214608"},{"type":"electronic","value":"9783642214615"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21461-5_7","type":"book-chapter","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T09:25:36Z","timestamp":1307697936000},"page":"106-120","source":"Crossref","is-referenced-by-count":3,"title":["A Framework for Verifying Data-Centric Protocols"],"prefix":"10.1007","author":[{"given":"Yuxin","family":"Deng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Grumbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Fran\u00e7ois","family":"Monin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","first-page":"104","volume-title":"POPL 2001","author":"M. Abadi","year":"2001","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL 2001, vol.\u00a036, pp. 104\u2013115. ACM, New York (2001)"},{"issue":"4","key":"7_CR2","doi-asserted-by":"publisher","first-page":"363","DOI":"10.3233\/JCS-2009-0339","volume":"17","author":"B. Blanchet","year":"2009","unstructured":"Blanchet, B.: Automatic Verification of Correspondences for Security Protocols. Journal of Computer Security\u00a017(4), 363\u2013434 (2009)","journal-title":"Journal of Computer Security"},{"key":"7_CR3","unstructured":"Cast\u00e9ran, P., Filou, V.: Tasks, Types and Tactics for Local Computation Systems. Studia Informatica Universalis (to appear, 2011)"},{"key":"7_CR4","volume-title":"Parallel program design: a foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M.: Parallel program design: a foundation. Addison-Wesley Longman Publishing Co., Inc., Amsterdam (1988)"},{"key":"7_CR5","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/32.663997","volume":"24","author":"B. Chetali","year":"1998","unstructured":"Chetali, B.: Formal Verification of Concurrent Programs Using the Larch Prover. IEEE Transactions on Software Engineering\u00a024, 46\u201362 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"7_CR6","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: The Concurrency Workbench: A semantics-based tool for the verification of concurrency systems. ACM Transactions on Programming Languages and Systems\u00a015(1), 36\u201372 (1993)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR7","unstructured":"Deng, Y., Grumbach, S., Monin, J.-F.: Coq Script for Netlog Protocols, http:\/\/www-verimag.imag.fr\/~monin\/Proof\/NetlogCoq\/netlogcoq.tar.gz"},{"key":"7_CR8","unstructured":"Deng, Y., Grumbach, S., Monin, J.-F.: Verifying Declarative Netlog Protocols with Coq: a First Experiment. Research Report 7511, INRIA (2011)"},{"key":"7_CR9","first-page":"201","volume-title":"TASE 2009","author":"Y. Deng","year":"2009","unstructured":"Deng, Y., Monin, J.-F.: Verifying Self-stabilizing Population Protocols with Coq. In: TASE 2009, pp. 201\u2013208. IEEE Computer Society, Los Alamitos (2009)"},{"key":"7_CR10","first-page":"246","volume-title":"ICSE 1992","author":"J.-C. Fernandez","year":"1992","unstructured":"Fernandez, J.-C., Garavel, H., Mounier, L., Rasse, A., Rodriguez, C., Sifakis, J.: A toolbox for the verification of LOTOS programs. In: ICSE 1992, pp. 246\u2013259. ACM, New York (1992)"},{"issue":"1","key":"7_CR11","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/357195.357200","volume":"5","author":"R.G. Gallager","year":"1983","unstructured":"Gallager, R.G., Humblet, P.A., Spira, P.M.: A Distributed Algorithm for Minimum-Weight Spanning Trees. ACM Trans. Program. Lang. Syst.\u00a05(1), 66\u201377 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR12","unstructured":"Gim\u00e9nez, E.: A Calculus of Infinite Constructions and its application to the verification of communicating systems. PhD thesis, ENS Lyon (1996)"},{"volume-title":"Formal Description Techniques IX: Theory, application and tools, IFIP TC6 WG6.1, IFIP Conference Proceedings","year":"1996","key":"7_CR13","unstructured":"Gotzhein, R., Bredereke, J. (eds.): Formal Description Techniques IX: Theory, application and tools, IFIP TC6 WG6.1, IFIP Conference Proceedings, vol.\u00a069. Chapman and Hall, Boca Raton (1996)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-11503-5_9","volume-title":"Practical Aspects of Declarative Languages","author":"S. Grumbach","year":"2010","unstructured":"Grumbach, S., Wang, F.: Netlog, a Rule-Based Language for Distributed Programming. In: Carro, M., Pe\u00f1a, R. (eds.) PADL 2010. LNCS, vol.\u00a05937, pp. 88\u2013103. Springer, Heidelberg (2010)"},{"issue":"1","key":"7_CR15","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s001650050035","volume":"11","author":"W.H. Hesselink","year":"1999","unstructured":"Hesselink, W.H.: The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract. Formal Asp. Comput.\u00a011(1), 45\u201355 (1999)","journal-title":"Formal Asp. Comput."},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/BFb0105409","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Heyd","year":"1996","unstructured":"Heyd, B., Cr\u00e9gut, P.: A Modular Coding of UNITY in COQ. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 251\u2013266. Springer, Heidelberg (1996)"},{"key":"7_CR17","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"issue":"3","key":"7_CR18","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1109\/32.4654","volume":"14","author":"C. Jard","year":"1988","unstructured":"Jard, C., Monin, J.F., Groz, R.: Development of Veda, a Prototyping Tool for Distributed Algorithms. IEEE Trans. Softw. Eng.\u00a014(3), 339\u2013352 (1988)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"7_CR19","first-page":"159","volume-title":"WIFT 1995","author":"C. Kirkwood","year":"1995","unstructured":"Kirkwood, C., Thomas, M.: Experiences with specification and verification in LOTOS: a report on two case studies. In: WIFT 1995, p. 159. IEEE Computer Society Press, Los Alamitos (1995)"},{"issue":"3","key":"7_CR20","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst.\u00a016(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"L\u00e5ngbacka, T.: A HOL Formalisation of the Temporal Logic of Actions. In: TPHOL 1994, pp. 332\u2013345. Springer, Heidelberg (1994)","DOI":"10.1007\/3-540-58450-1_52"},{"key":"7_CR22","first-page":"42","volume-title":"POPL 2006","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL 2006, pp. 42\u201354. ACM, New York (2006)"},{"key":"7_CR23","first-page":"63","volume-title":"PRESTO 2008","author":"C. Liu","year":"2008","unstructured":"Liu, C., Mao, Y., Oprea, M., Basu, P., Loo, B.T.: A declarative perspective on adaptive manet routing. In: PRESTO 2008, pp. 63\u201368. ACM, New York (2008)"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Loo, B.T., Condie, T., Garofalakis, M.N., Gay, D.E., Hellerstein, J.M., Maniatis, P., Ramakrishnan, R., Roscoe, T., Stoica, I.: Declarative networking: language, execution and optimization. In: ACM SIGMOD 2006 (2006)","DOI":"10.1145\/1142473.1142485"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Loo, B.T., Hellerstein, J.M., Stoica, I., Ramakrishnan, R.: Declarative routing: extensible routing with declarative queries. In: ACM SIGCOMM 2005 (2005)","DOI":"10.1145\/1080091.1080126"},{"key":"7_CR26","volume-title":"Distributed Algorithms","author":"N.A. Lynch","year":"1996","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1996)"},{"key":"7_CR27","first-page":"219","volume":"2","author":"N.A. Lynch","year":"1989","unstructured":"Lynch, N.A., Tuttle, M.R.: An introduction to input\/output automata. CWI Quarterly\u00a02, 219\u2013246 (1989)","journal-title":"CWI Quarterly"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/BFb0097797","volume-title":"Types for Proofs and Programs","author":"J.-F. Monin","year":"1998","unstructured":"Monin, J.-F.: Proving a real time algorithm for ATM in Coq. In: Gim\u00e9nez, E. (ed.) TYPES 1996. LNCS, vol.\u00a01512, pp. 277\u2013293. Springer, Heidelberg (1998)"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/11864219_9","volume-title":"Distributed Computing","author":"Y. Moses","year":"2006","unstructured":"Moses, Y., Shimony, B.: A New Proof of the GHS Minimum Spanning Tree Algorithm. In: Dolev, S. (ed.) DISC 2006. LNCS, vol.\u00a04167, pp. 120\u2013135. Springer, Heidelberg (2006)"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/3-540-61780-9_72","volume-title":"Types for Proofs and Programs","author":"C. Paulin-Mohring","year":"1996","unstructured":"Paulin-Mohring, C.: Circuits as Streams in Coq: Verification of a Sequential Multiplier. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 216\u2013230. Springer, Heidelberg (1996)"},{"issue":"1","key":"7_CR31","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/343369.343370","volume":"1","author":"L.C. Paulson","year":"2000","unstructured":"Paulson, L.C.: Mechanizing UNITY in Isabelle. ACM Trans. Comput. Logic\u00a01(1), 3\u201332 (2000)","journal-title":"ACM Trans. Comput. Logic"},{"key":"7_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/BFb0054188","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Regensburger","year":"1998","unstructured":"Regensburger, F., Barnard, A.: Formal Verification of SDL Systems at the Siemens Mobile Phone Department. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 439\u2013455. Springer, Heidelberg (1998)"},{"key":"7_CR33","volume-title":"Model-checking CSP","author":"A.W. Roscoe","year":"1994","unstructured":"Roscoe, A.W.: Model-checking CSP, ch. 21. Prentice-Hall, Englewood Cliffs (1994)"},{"key":"7_CR34","unstructured":"Shahrier, S.M., Jenevein, R.M.: SDL Specification and Verification of a Distributed Access Generic optical Network Interface for SMDS Networks. Technical report, University of Texas at Austin (1997)"},{"key":"7_CR35","first-page":"267","volume-title":"FORTE XI \/ PSTV XVIII 1998","author":"M. T\u00f6r\u00f6","year":"1998","unstructured":"T\u00f6r\u00f6, M., Zhu, J., Leung, V.C.M.: SDL specification and verification of universal personal computing: with Object GEODE. In: FORTE XI \/ PSTV XVIII 1998, pp. 267\u2013282. Kluwer, B.V., Dordrecht (1998)"},{"key":"7_CR36","volume-title":"Using Formal Description Techniques: An Introduction to Estelle, Lotos, and SDL","author":"K.J. Turner","year":"1993","unstructured":"Turner, K.J.: Using Formal Description Techniques: An Introduction to Estelle, Lotos, and SDL. John Wiley & Sons, Inc., Chichester (1993)"},{"key":"7_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-540-92995-6_5","volume-title":"Practical Aspects of Declarative Languages","author":"A. Wang","year":"2008","unstructured":"Wang, A., Basu, P., Loo, B.T., Sokolsky, O.: Declarative Network Verification. In: Gill, A., Swift, T. (eds.) PADL 2009. LNCS, vol.\u00a05418, pp. 61\u201375. Springer, Heidelberg (2008)"},{"key":"7_CR38","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/62546.62552","volume-title":"Proceedings of the seventh annual ACM Symposium on Principles of distributed computing, PODC 1988","author":"J.L. Welch","year":"1988","unstructured":"Welch, J.L., Lamport, L., Lynch, N.: A lattice-structured proof of a minimum spanning. In: Proceedings of the seventh annual ACM Symposium on Principles of distributed computing, PODC 1988, pp. 28\u201343. ACM, New York (1988)"},{"key":"7_CR39","first-page":"533","volume-title":"FORTE 1989","author":"J.-P. Wu","year":"1990","unstructured":"Wu, J.-P., Chanson, S.T.: Translation from LOTOS and Estelle Specifications to Extended Transition System and its Verification. In: FORTE 1989, pp. 533\u2013549. North-Holland Publishing Co., Amsterdam (1990)"},{"key":"7_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/3-540-48213-X_26","volume-title":"SDL 2001: Meeting UML","author":"W. Zhang","year":"2001","unstructured":"Zhang, W.: Applying SDL Specifications and Tools to the Verification of Procedures. In: Reed, R., Reed, J. (eds.) SDL 2001. LNCS, vol.\u00a02078, pp. 421\u2013438. Springer, Heidelberg (2001)"}],"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-21461-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T12:20:13Z","timestamp":1560255613000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21461-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214608","9783642214615"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21461-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}