{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,10,20]],"date-time":"2022-10-20T00:30:39Z","timestamp":1666225839679},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,6,9]],"date-time":"2006-06-09T00:00:00Z","timestamp":1149811200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2006,7]]},"DOI":"10.1007\/s10703-006-0004-3","type":"journal-article","created":{"date-parts":[[2006,6,8]],"date-time":"2006-06-08T12:10:26Z","timestamp":1149768626000},"page":"1-31","source":"Crossref","is-referenced-by-count":10,"title":["Cones and foci: A mechanical framework for protocol verification"],"prefix":"10.1007","volume":"29","author":[{"given":"Wan","family":"Fokkink","sequence":"first","affiliation":[]},{"given":"Jun","family":"Pang","sequence":"additional","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,6,9]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow, Term rewriting and all that, Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"B. Badban, W.J. Fokkink, J.F. Groote, J. Pang, and J.C. van de Pol, \u201cVerification of a sliding window protocol in \u03bcCRL and PVS,\u201d Form. Asp. Comp., Vol. 17, pp. 342\u2013388, 2005.","DOI":"10.1007\/s00165-005-0070-0"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"J.C.M. Baeten J.A. Bergstra, and J.W. Klop, \u201cOn the consistency of Koomen's fair abstraction rule,\u201d Theor. Comp. Sci., Vol. 51, pp. 129\u2013176, 1987.","DOI":"10.1016\/0304-3975(87)90052-1"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"J.C.M. Baeten and W.P. Weijland, Process Algebra, vol. 18 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1990.","DOI":"10.1017\/CBO9780511624193"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"T. Basten, \u201cBranching bisimilarity is an equivalence indeed!,\u201d Inform. Proc. Lett., Vol. 58, pp. 141\u2013147, 1996.","DOI":"10.1016\/0020-0190(96)00034-8"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"J.A. Bergstra and J.W. Klop, \u201cAlgebra of communicating processes with abstraction,\u201d Theor. Comp. Sci., Vol. 37, pp. 77\u2013121, 1985.","DOI":"10.1016\/0304-3975(85)90088-X"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"M.A. Bezem and J.F. Groote, \u201cInvariants in process algebra with data,\u201d in Proc. 5th Conference on Concurrency Theory, LNCS 836, Springer, 1994, pp. 401\u2013416.","DOI":"10.1007\/978-3-540-48654-1_30"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"S.C.C. Blom, W.J. Fokkink, J.F. Groote, I.A. van Langevelde, B. Lisser, and J.C. van de Pol,\u201c \u03bcCRL: A toolset for analysing algebraic specifications,\u201d in Proc. 13th Conference on Computer Aided Verification, Springer, LNCS 2102, 2001, pp. 250\u2013254.","DOI":"10.1007\/3-540-44585-4_23"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"S.C.C. Blom and J.C. van de Pol, \u201cState space reduction by proving confluence,\u201d in Proc. 14th Conference on Computer Aided Verification, Springer, LNCS 2404, 2002, pp. 596\u2013609.","DOI":"10.1007\/3-540-45657-0_50"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra, Parallel Program Design. A Foundation, Addison Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"A. Cimatti, F. Giunchiglia, P. Pecchiari, B. Pietra, J. Profeta, D. Romano, P. Traverso, and B. Yu, \u201cA provably correct embedded verifier for the certification of safety critical software,\u201d in Proc. 9th Conference on Computer Aided Verification, Springer, LNCS 1254, 1997, pp. 202\u2013213.","DOI":"10.1007\/3-540-63166-6_21"},{"key":"4_CR12","unstructured":"E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking, MIT Press, 2000."},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"B. Courcelle, \u201cRecursive applicative program schemes\u201d in Handbook of Theoretical Computer Science, Volume B, Formal Methods and Semantics, Elsevier, 1990, pp. 459\u2013492.","DOI":"10.1016\/B978-0-444-88074-1.50014-7"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"W.J. Fokkink, J.F. Groote, J. Pang, B. Badban, and J.C. van de Pol, \u201cVerifying a sliding window protocol in \u03bcCRL,\u201d in Proc. 10th Conference on Algebraic Methodology and Software Technology, Springer, LNCS 3116, 2004, pp. 148\u2013163.","DOI":"10.1007\/978-3-540-27815-3_15"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"W.J. Fokkink and J. Pang, \u201cCones and foci for protocol verification revisited,\u201d in Proc. 6th Conference on Foundations of Software Science and Computation Structures, Springer, LNCS 2620, 2003, pp. 267\u2013281.","DOI":"10.1007\/3-540-36576-1_17"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"W.J. Fokkink and J.C. van de Pol, \u201cSimulation as a correct transformation of rewrite systems,\u201d in Proceedings of 22nd Symposium on Mathematical Foundations of Computer Science, Springer, LNCS 1295, 1997, pp. 249\u2013258.","DOI":"10.1007\/BFb0029968"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"L.-\u212b. Fredlund, J.F. Groote, and H.P. Korver, \u201cFormal verification of a leader election protocol in process algebra,\u201d Theor. Comp. Sci., Vol. 177, pp. 459\u2013486, 1997.","DOI":"10.1016\/S0304-3975(96)00256-3"},{"key":"4_CR18","unstructured":"H. Garavel, F. Lang, and R. Mateescu, \u201cAn overview of CADP 2001,\u201d Technical Report RT-0254, INRIA Rhone-Alpes, 2001."},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"R.J. van Glabbeek and W.P. Weijland, \u201cBranching time and abstraction in bisimulation semantics,\u201d J. ACM, Vol. 43, pp. 555\u2013600, 1996.","DOI":"10.1145\/233551.233556"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"M. Glusman and S. Katz, \u201cA mechanized proof environment for the convenient computations proof method,\u201d Form. Meth. Syst. Des., Vol. 23, No. 2, pp. 115\u2013142, 2003.","DOI":"10.1023\/A:1024746015231"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"W. Goerigk and F. Simon, \u201cTowards rigorous compiler implementation verification,\u201d in Collaboration between Human and Artificial Societies, Coordination and Agent-Based Distributed Computing, Springer, LNCS 1624, 1999, pp. 62\u201373.","DOI":"10.1007\/10703260_4"},{"key":"4_CR22","unstructured":"J.F. Groote and B. Lisser, \u201cComputer assisted manipulation of algebraic process specifications,\u201d in Proc. 3rd Workshop on Verification and Computational Logic, Technical Report DSSE-TR-2002-5. Department of Electronics and Computer Science, University of Southampton, 2002."},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"J.F. Groote, F. Monin, and J.C. van de Pol, \u201cChecking verifications of protocols and distributed systems by computer,\u201d in Proc. 9th Conference on Concurrency Theory, Springer, LNCS 1466, 1998, pp. 629\u2013655.","DOI":"10.1007\/BFb0055652"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"J.F. Groote and A. Ponse, \u201cThe syntax and semantics of \u03bcCRL,\u201d in Proc. 1st Workshop on the Algebra of Communicating Processes, Workshops in Computing Series, Springer, 1995, pp. 26\u201362.","DOI":"10.1007\/978-1-4471-2120-6_2"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"J.F. Groote A. Ponse, and Y.S. Usenko, \u201cLinearization in parallel pCRL,\u201d J. Logic Algeb. Prog., Vol. 48, pp. 39\u201372, 2001.","DOI":"10.1016\/S1567-8326(01)00005-4"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"J.F. Groote and M. Reniers, \u201cAlgebraic process verification,\u201d in J.A. Bergstra, A. Ponse, and S.A. Smolka (Eds.), Handbook of Process Algebra, Elsevier, 2001, pp. 1151\u20131208.","DOI":"10.1016\/B978-044482830-9\/50035-7"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"J.F. Groote and J. Springintveld, \u201cFocus points and convergent process operators. A proof strategy for protocol verification,\u201d J. Logic Algeb. Prog., Vol. 49, pp. 31\u201360, 2001.","DOI":"10.1016\/S1567-8326(01)00010-8"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"J.F. Groote and F.W. Vaandrager, \u201cAn efficient algorithm for branching bisimulation and stuttering equivalence,\u201d in Proc. 17th Colloquium on Automata, Languages and Programming, Springer, LNCS 443, 1990, pp. 626\u2013638.","DOI":"10.1007\/BFb0032063"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"J.F. Groote and J.J. van Wamel, \u201cThe parallel composition of uniform processes with data\u201d Theor. Comp. Sci., Vol. 266, pp. 631\u2013652, 2001.","DOI":"10.1016\/S0304-3975(00)00324-8"},{"key":"4_CR30","unstructured":"B. Jonsson, Compositional Verification of Distributed Systems. PhD thesis, Department of Computer Science, Uppsala University, 1987."},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"C.P.J. Koymans and J.C. Mulder, \u201cA modular approach to protocol verification using process algebra\u201d in Applications of Process Algebra, Cambridge Tracts in Theoretical Computer Science 17, Cambridge University Press, 1990, pp. 261\u2013306.","DOI":"10.1017\/CBO9780511608841.012"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"L. Lamport, \u201cThe temporal logic of actions,\u201d ACM Trans. Prog. Lang. Syst., Vol. 16, No. 3, pp. 872\u2013923, 1994.","DOI":"10.1145\/177492.177726"},{"key":"4_CR33","unstructured":"J. Loeckx, H.-D. Ehrich, and M. Wolf, Specification of Abstract Data Types, Wiley\/Teubner, 1996."},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"N.A. Lynch and M.R. Tuttle, \u201cHierarchical correctness proofs for distributed algorithms,\u201d in Proc. 6th ACM Symposium on Principles of Distributed Computing, ACM, 1987, pp. 137\u2013151.","DOI":"10.1145\/41840.41852"},{"key":"4_CR35","unstructured":"N.A. Lynch and M.R. Tuttle, \u201cAn introduction to input\/output automata,\u201d CWI Quarterly, Vol. 2, No. 3, pp. 219\u2013246, 1989."},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"N.A. Lynch and F.W. Vaandrager, \u201cForward and backward simulations. Part I: Untimed systems,\u201d Inform. Comp., Vol. 121, pp. 214\u2013233, 1995.","DOI":"10.1006\/inco.1995.1134"},{"key":"4_CR37","unstructured":"S. Merz, \u201cMechanizing TLA in Isabelle,\u201d in Proc. Workshop on Verification in New Orientations, University of Maribor, 1995, pp. 54\u201374."},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"O. M\u00fcller and T. Nipkow, \u201cTraces of I\/O-automata in Isabelle\/HOLCF,\u201d in Proc. 7th Conference on Theory and Practice of Software Development, Springer, LNCS 1214, 1997, pp. 580\u2013594.","DOI":"10.1007\/BFb0030627"},{"key":"4_CR39","unstructured":"G. Necula, \u201cTranslation validation for an optimizing compiler,\u201d in Proc. 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation, SIGPLAN Notices, ACM, Vol. 35, pp. 83\u201394, 2000."},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"T. Nipkow and L. Prensa Nieto, \u201cOwicki\/Gries in Isabelle\/HOL\u201d in Proc. 2nd Conference on Fundamental Approaches in Software Engineering, Springer, LNCS 1577, 1999, pp. 188\u2013203.","DOI":"10.1007\/978-3-540-49020-3_13"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"T. Nipkow and K. Slind, \u201cI\/O automata in Isabelle\/HOL,\u201d in Proc. 2nd Workshop on Types for Proofs and Programs, Springer, LNCS 996, 1994, pp. 101\u2013119.","DOI":"10.1007\/3-540-60579-7_6"},{"key":"4_CR42","doi-asserted-by":"crossref","unstructured":"T. Nipkow, L.C. Paulson, and M. Wenzel, Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, Springer, LNCS 2283, 2002.","DOI":"10.1007\/3-540-45949-9"},{"key":"4_CR43","doi-asserted-by":"crossref","unstructured":"S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas, \u201cPVS: Combining specification, proof checking, and model checking,\u201d in Proc. 8th Conference on Computer-Aided Verification, Springer, LNCS 1102, 1996, pp. 411\u2013414.","DOI":"10.1007\/3-540-61474-5_91"},{"key":"4_CR44","doi-asserted-by":"crossref","unstructured":"L.C. Paulson, \u201cMechanizing UNITY in Isabelle\u201d ACM Transactions on Computational Logic, Vol. 1, No. 1, pp. 3\u201332, 2000.","DOI":"10.1145\/343369.343370"},{"key":"4_CR45","doi-asserted-by":"crossref","unstructured":"A. Pnueli, M. Siegel, and E. Singerman, \u201cTranslation validation,\u201d in Proc. 4th Conference on Tools and Algorithms for Construction and Analysis of Systems, Springer, LNCS 1384, 1998, pp. 151\u2013166.","DOI":"10.1007\/BFb0054170"},{"key":"4_CR46","unstructured":"J.C. van de Pol, \u201cA prover for the \u03bcCRL toolset with applications\u2014version 0.1,\u201d Technical Report SEN-R0106, CWI Amsterdam, 2001."},{"key":"4_CR47","doi-asserted-by":"crossref","unstructured":"C. R\u00f6ckl and J. Esparza, \u201cProof-checking protocols using bisimulations,\u201d in Proc. 10th Conference on Concurrency Theory, Springer, LNCS 1664, 1999, pp. 525\u2013540.","DOI":"10.1007\/3-540-48320-9_36"},{"key":"4_CR48","doi-asserted-by":"crossref","unstructured":"C. Shankland and M.B. van der Zwaag, \u201cThe tree identify protocol of IEEE 1394 in \u03bcCRL,\u201d Form. Asp. Comp., Vol. 10, pp. 509\u2013531,1998.","DOI":"10.1007\/s001650050030"},{"key":"4_CR49","unstructured":"Y.S. Usenko, \u201cLinearization of \u03bcCRL specifications (extended abstract),\u201d in Proc. 3rd Workshop on Verification and Computational Logic, Technical Report DSSE-TR-2002-5. Department of Electronics and Computer Science, University of Southampton, 2002."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0004-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-0004-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0004-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T18:01:02Z","timestamp":1559239262000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-0004-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,6,9]]},"references-count":49,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,7]]}},"alternative-id":["4"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-0004-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,6,9]]}}}