{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:40:02Z","timestamp":1748072402801,"version":"3.41.0"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2002,4,1]],"date-time":"2002-04-01T00:00:00Z","timestamp":1017619200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,4,1]],"date-time":"2002-04-01T00:00:00Z","timestamp":1017619200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Automated Software Engineering"],"published-print":{"date-parts":[[2002,4]]},"DOI":"10.1023\/a:1014530313153","type":"journal-article","created":{"date-parts":[[2002,12,28]],"date-time":"2002-12-28T20:42:43Z","timestamp":1041108163000},"page":"137-150","source":"Crossref","is-referenced-by-count":11,"title":["Mark, a Reasoning Kit for Mobility"],"prefix":"10.1007","volume":"9","author":[{"given":"Gianluigi","family":"Ferrari","sequence":"first","affiliation":[]},{"given":"C.","family":"Montangero","sequence":"additional","affiliation":[]},{"given":"L.","family":"Semini","sequence":"additional","affiliation":[]},{"given":"S.","family":"Semprini","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"398750_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1999","unstructured":"Abadi, M. and Gordon, A. 1999. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148(1):1\u201370.","journal-title":"Information and Computation"},{"key":"398750_CR2","series-title":"The Java Series","volume-title":"The Java Programming Language","author":"K. Arnold","year":"1998","unstructured":"Arnold, K. and Gosling, J. 1998. The Java Programming Language, 2nd edn. The Java Series. Reading, MA: Addison-Wesley.","edition":"2nd edn."},{"key":"398750_CR3","first-page":"233","volume":"426","author":"M. Burrows","year":"1989","unstructured":"Burrows, M., Abadi, M., and Needham, R. 1989. A logic of authentication. Proceedings of the Royal Society, Series A, 426:233\u2013271. In shorthened form also in ACM Transactions on Computer Systems, 8(1):18\u201336, 1990.","journal-title":"Proceedings of the Royal Society, Series A"},{"key":"398750_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/3-540-48523-6_20","volume-title":"26th Colloquium on Automata, Languages and Programming (ICALP)","author":"L. Cardelli","year":"1999","unstructured":"Cardelli, L., Ghelli, G., and Gordon, A.D. 1999. Mobility types for mobile ambients. In J. Wiederman, P. van Emde Boas, and M. Nielsen, editors, 26th Colloquium on Automata, Languages and Programming (ICALP), Prague, Czech Republic, July 1999, Vol. 1644 of Lecture Notes in Computer Science. Berlin: Springer-Verlag, pp. 230\u2013239."},{"key":"398750_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/BFb0053547","volume-title":"Foundations of Software Science and Computational Structures","author":"L. Cardelli","year":"1998","unstructured":"Cardelli, L. and Gordon, A.D. 1998. Mobile ambients. In M. Nivat, editor, Foundations of Software Science and Computational Structures, Vol. 1378 of Lecture Notes in Computer Science. Berlin: Springer-Verlag, pp. 140\u2013155."},{"key":"398750_CR6","volume-title":"Parallel Program Design: A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M. and Misra, J. 1988. Parallel Program Design: A Foundation. Reading, MA: Addison-Wesley."},{"key":"398750_CR7","series-title":"Lecture Notes in Computer Science","first-page":"93","volume-title":"Mobile Object Systems: Towards the Programmable Internet","author":"G. Cugola","year":"1997","unstructured":"Cugola, G., Ghezzi, C., Picco, G.P., and Vigna, G. 1997. Analyzing mobile code languages. In Mobile Object Systems: Towards the Programmable Internet,Vol. 1222 of Lecture Notes in Computer Science. Berlin: Springer-Verlag, pp. 93\u2013110."},{"issue":"5","key":"398750_CR8","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1109\/32.685256","volume":"24","author":"R. De Nicola","year":"1998","unstructured":"De Nicola, R., Ferrari, G., and Pugliese, R. 1998. A kernel language for agents interaction and mobility. IEEE Transactions on Software Engineering, 24(5):315\u2013330.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"398750_CR9","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1016\/S0304-3975(99)00232-7","volume":"240","author":"R. De Nicola","year":"2000","unstructured":"De Nicola, R., Ferrari, G., Pugliese, R., and Venneri, B. 2000. Types for access control. Theoretical Computer Science, 240(1):215\u2013254.","journal-title":"Theoretical Computer Science"},{"key":"398750_CR10","unstructured":"Ferrari, G., Montangero, C., Semini, L., and Semprini, S. (2000a). Multiple security policies in Mobadtl. In Proc. Workshop on Issues in the Theory of Security (WITS'00), Geneva, 78 July 2000."},{"key":"398750_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-44522-6","volume-title":"Proc. Limassol, Cyprus, Sept. 2000, 4th Int. Conf. on Coordination Models and Languages, COORDINATION'00","author":"G. Ferrari","year":"2000","unstructured":"Ferrari, G., Montangero, C., Semini, L., and Semprini, S. (2000b). Mobile agents coordination in Mobadtl. In A. Porto and G.-C. Roman, editors, Proc. Limassol, Cyprus, Sept. 2000, 4th Int. Conf. on Coordination Models and Languages, COORDINATION'00, Vol. 1906 of Lecture Notes in Computer Science. Berlin: Springer-Verlag."},{"key":"398750_CR12","doi-asserted-by":"crossref","unstructured":"Focardi, R., Gorrieri, R., and Martinelli, F. 2000. Non-interference for the analysis of cryptographic protocols. In Proc. ICALP'2000, LNCS.","DOI":"10.1007\/3-540-45022-X_31"},{"key":"398750_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1007\/3-540-61604-7_67","volume-title":"Proc. CONCUR '96: Concurrency Theory, 7th International Conference","author":"C. Fournet","year":"1996","unstructured":"Fournet, C., Gonthier, G., L\u00e9vy, J.-J., Maranget, L., and R\u00e9my, D. 1996. A calculus of mobile agents. In U. Montanari and V. Sassone, editors, Proc. CONCUR '96: Concurrency Theory, 7th International Conference, Pisa, Aug. 1996. Vol. 1119 of Lecture Notes in Computer Science. Berlin: Springer-Verlag, pp. 406\u2013421."},{"issue":"5","key":"398750_CR14","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1109\/32.685258","volume":"24","author":"A. Fuggetta","year":"1998","unstructured":"Fuggetta, A., Picco, G.P., and Vigna, G. 1998. Understanding code mobility. IEEE Transactions on Software Engineering, 24(5):342\u2013361.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"398750_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/BFb0055133","volume-title":"Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs '98","author":"D. Griffioen","year":"1998","unstructured":"Griffioen, D. and Huisman, M. 1998. A comparison of PVS and Isabelle\/HOL. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs '98, Vol. 1479 of Lecture Notes in Computer Science, Canberra, Australia, Sept. 1998. Berlin: Springer-Verlag, pp. 123\u2013142."},{"key":"398750_CR16","series-title":"Electronic Notes on Theoretical Computer Science","first-page":"3","volume-title":"Proc. HLCL '98: High-Level Concurrent Languages","author":"M. Hennessy","year":"1998","unstructured":"Hennessy, M. and Riely, J. 1998. Resource access control in systems of mobile agents. In U. Nestmann and B.C. Pierce, editors, Proc. HLCL '98: High-Level Concurrent Languages, Vol. 16.3 of Electronic Notes on Theoretical Computer Science. Nice, France, Sept. 1998. New York: Elsevier Science, pp. 3\u201317."},{"key":"398750_CR17","volume-title":"Programming and Deploying Java Mobile Agents with Aglets","author":"D.B. Lange","year":"1998","unstructured":"Lange, D.B. and Oshima, M. 1998. Programming and Deploying Java Mobile Agents with Aglets. Reading, MA: Addison-Wesley."},{"key":"398750_CR18","first-page":"352","volume-title":"Proc. 27th Annual ACM Symp. on Principles of Programming Languages","author":"F. Levi","year":"2000","unstructured":"Levi, F. and Sangiorgi, D. 2000. Controlling interference in Ambients. In Proc. 27th Annual ACM Symp. on Principles of Programming Languages, Boston, Jan. 2000. New York: ACM Press, pp. 352\u2013364."},{"key":"398750_CR19","doi-asserted-by":"crossref","unstructured":"Marrero, W., Clarke, E.M., and Jha, S. 1997. Model checking for security protocols. Technical Report CMU-SCS\u201397\u2013139, Carnegie Mellon University.","DOI":"10.21236\/ADA327281"},{"issue":"2","key":"398750_CR20","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1109\/32.666824","volume":"24","author":"P.J. McCann","year":"1998","unstructured":"McCann, P.J. and Roman, G.-C. 1998. Compositional programming abstractions for mobile computing. IEEE Transactions on Software Engineering, 24(2):97\u2013110.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"398750_CR21","first-page":"141","volume-title":"10th IEEE Computer Security Foundations Workshop","author":"J.C. Mitchell","year":"1997","unstructured":"Mitchell, J.C., Mitchell, M., and Ster, U. 1997. Automated analysis of cryptographic protocols using Mur\u03d5. In 10th IEEE Computer Security Foundations Workshop. Piscataway, NJ: IEEE Press, pp. 141\u2013151."},{"key":"398750_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/3-540-48919-3_10","volume-title":"Proc. 3nd Int. Conf. on Coordination Models and Languages","author":"C. Montangero","year":"1999","unstructured":"Montangero, C. and Semini, L. 1999. Composing specifications for coordination. In P. Ciancarini and A. Wolf, editors, Proc. 3nd Int. Conf. on Coordination Models and Languages, Vol. 1594 of Lecture Notes in Computer Science. Amsterdam, April 1999. Berlin: Springer-Verlag, pp. 118\u2013133."},{"key":"398750_CR23","first-page":"106","volume-title":"Proc. 24th ACM Symp. on Priciples of Programming Languages","author":"G. Necula","year":"1997","unstructured":"Necula, G. 1997. Proof-carrying code. In Proc. 24th ACM Symp. on Priciples of Programming Languages. New York: ACM Press, pp. 106\u2013119."},{"key":"398750_CR24","unstructured":"Owre, S., Rushby, J., and Shankar, N. The PVS specification and verification system. Available at http:\/\/pvs.csl.sri.com\/."},{"key":"398750_CR25","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1109\/CSFW.1997.596788","volume-title":"10th IEEE Computer Security Foundations Workshop","author":"L.C. Paulson","year":"1997","unstructured":"Paulson, L.C. 1997. Proving properties of security protocols by induction. In 10th IEEE Computer Security Foundations Workshop. New York: IEEE Press, pp. 70\u201383."},{"key":"398750_CR26","unstructured":"Paulson, L. and Nipkow, T. Isabelle. Available at www.cl.cam.ac.uk\/Research\/HVG\/Isabelle\/."},{"key":"398750_CR27","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/S0167-6423(98)00021-5","volume":"34","author":"L. Semini","year":"1999","unstructured":"Semini, L. and Montangero, C. 1999. A refinement calculus for tuple spaces. Science of Computer Programming, 34:79\u2013140.","journal-title":"Science of Computer Programming"},{"key":"398750_CR28","volume-title":"Proc. Computer Security Foundations Workshop 12, CSFW-12","author":"P. Sewell","year":"1999","unstructured":"Sewell, P. and Vitek, J. 1999. Secure composition of insecure components. In Proc. Computer Security Foundations Workshop 12, CSFW-12. New York: IEEE."},{"key":"398750_CR29","series-title":"Lecture Notes in Computer Science","volume-title":"Proc.Workshop on Internet Programming Languages","author":"J. Vitek","year":"1998","unstructured":"Vitek, J. and Castagna, G. 1998. Towards a calculus of secure mobile computations. In Proc.Workshop on Internet Programming Languages,Vol. 1686 of Lecture Notes in Computer Science. Chicago, Illinois, May 1998. Berlin: Springer-Verlag."}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1014530313153.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1014530313153\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1014530313153.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:00:14Z","timestamp":1748070014000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1014530313153"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,4]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,4]]}},"alternative-id":["398750"],"URL":"https:\/\/doi.org\/10.1023\/a:1014530313153","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"type":"print","value":"0928-8910"},{"type":"electronic","value":"1573-7535"}],"subject":[],"published":{"date-parts":[[2002,4]]}}}