{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:21:16Z","timestamp":1725664876236},"publisher-location":"Berlin, Heidelberg","reference-count":88,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540625032"},{"type":"electronic","value":"9783540680529"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62503-8_1","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:39:43Z","timestamp":1330295983000},"page":"1-21","source":"Crossref","is-referenced-by-count":2,"title":["Logical and operational methods in the analysis of programs and systems"],"prefix":"10.1007","author":[{"given":"F.","family":"Nielson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Cousot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Dam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Degano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Jouvelot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Mycroft","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"B.","family":"Thomsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/3-540-59293-8_196","volume":"915","author":"R. Amadio","year":"1995","unstructured":"R. Amadio and M. Dam. Reasoning about higher-order processes. In Proc. CAAP'94, Lecture Notes in Computer Science, 915:202\u2013217, 1995.","journal-title":"Lecture Notes in Computer Science"},{"key":"1_CR2","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-61648-9_50","volume":"1135","author":"R. Amadio","year":"1996","unstructured":"R. Amadio and M. Dam. A modal theory of types for the \u03c0-calculus. In Proc. FTRTFT'96, Lecture Notes in Computer Science, 1135:347\u2013365, 1996.","journal-title":"Lecture Notes in Computer Science"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"H. Andersen, C. Stirling, and G. Winskel. A compositional proof system for the modal \u03bc-calculus. In Proc. LICS'94, 1994.","DOI":"10.1109\/LICS.1994.316076"},{"key":"1_CR4","unstructured":"J.-M Andreoli and R. Pareschi: \u201dLinear objects: Logical processes with built-in inheritance\u201d. In D.H.D. Warren and P. Szeredi, editors, 7th Int. Conf. Logic Programming. MIT Press, 1990."},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"J.-M Andreoli, R. Pareschi, L. Leth and B. Thomsen: \u201dTrue Concurrency Semantics for a Linear Logic Programming Language with Broadcast Communication\u201d. In proc. Conf. on Theory and Practice of Software Development (TAPSOFT'93), vol 668 of LNCS, pp. 182\u2013198. Springer Verlag, 1993.","DOI":"10.1007\/3-540-56610-4_64"},{"issue":"1","key":"1_CR6","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1145\/151233.151242","volume":"36","author":"J.-P. Banatre","year":"1993","unstructured":"J.-P. Banatre and D. Le Metayer. \u201dProgramming by multiset transformations. CACM, 36(1):98, 1993","journal-title":"CACM"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"A. Bianchi, S. Coluccini, P. Degano, and C. Priami. An efficient verifier of truly concurrent properties. In V. Malyshkin, editor, Proceedings of PaCT'95, LNCS 964, pages 36\u201350. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60222-4_95"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"C. Bodei, P. Degano, and C. Priami. Mobile processes with a distributed environment. In Proceedings of ICALP'96, LNCS 1099, pages 490\u2013501. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61440-0_153"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Roberta Borgia, Pierpaolo Degano, Corrado Priami, Lone Leth, and Bent Thomsen. Understanding mobile agents via a non-interleaving semantics for Facile. In R. Cousot and D.A. Schmidt, editors, Proceedings of SAS'96, LNCS 1145, pages 98\u2013112. Springer-Verlag, 1996. Extended version in European Computer-Industry Research Center Tech. Rep. ECRC-96-4, 1996.","DOI":"10.1007\/3-540-61739-6_36"},{"issue":"4","key":"1_CR10","doi-asserted-by":"crossref","first-page":"433","DOI":"10.3233\/FI-1988-11406","volume":"XI","author":"G. Boudol","year":"1988","unstructured":"G. Boudol and I. Castellani. A non-interleaving semantics for CCS based on proved transitions. Fundamenta Informaticae, XI(4):433\u2013452, 1988.","journal-title":"Fundamenta Informaticae"},{"key":"1_CR11","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. Proc. LICS'90, 1990."},{"key":"1_CR12","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/BFb0084787","volume":"630","author":"O. Burkart","year":"1992","unstructured":"O. Burkart and B. Steffen. Model checking for context-free processes. In Proc. CONCUR'92, Lecture Notes in Computer Science, 630:123\u2013137, 1992.","journal-title":"Lecture Notes in Computer Science"},{"key":"1_CR13","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0167-6423(86)90010-9","volume":"7","author":"G. L. Burn","year":"1986","unstructured":"G. L. Burn, C. Hankin, and S. Abramsky. Strictness Analysis for Higher-Order Functions. Science of Computer Programming, 7:249\u2013278, 1986.","journal-title":"Science of Computer Programming"},{"issue":"4","key":"1_CR14","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1016\/0167-8191(94)90032-9","volume":"20","author":"N. Carriero","year":"1994","unstructured":"N. Carriero, D. Gelernter, T. Mattson and A. Sherman. \u201dThe Linda alternative to message passing systems\u201d. Parallel Computing 20(4):633\u2013655, April 1994.","journal-title":"Parallel Computing"},{"key":"1_CR15","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/s002360050039","volume":"33","author":"A. Cau","year":"1996","unstructured":"A. Cau and P. Collette. Parallel composition of assumption-commitment specifications. Acta Informatica, 33:153\u2013176, 1996.","journal-title":"Acta Informatica"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics-based tool for the verification of concurrent systems. ACM Transaction on Programming Languages and Systems, pages 36\u201372, 1993.","DOI":"10.1145\/151646.151648"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"P. Cousot. Methods and logics for proving programs. In J. van Leeuwen, editor, Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science, chapter 15, pages 843\u2013993. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50020-2"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In 19th POPL, pages 83\u201394. ACM Press, 1992.","DOI":"10.1145\/143165.143184"},{"issue":"4","key":"1_CR19","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"P. Cousot and R. Cousot. Abstract interpretation frameworks. J. Logic and Comp., 2(4):511\u2013547, 1992.","journal-title":"J. Logic and Comp."},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Comparing the Galois connection and widening\/ narrowing approaches to abstract interpretation, invited paper. In M. Bruynooghe and M. Wirsing, editors, Proc. Int. Work. PLILP '92. LNCS 631, pages 269\u2013295. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55844-6_142"},{"key":"1_CR21","unstructured":"P. Cousot and R. Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages), invited paper. In Proc. 1994 ICCL, pages 95\u2013112. IEEE Comp. Soc. Press, 1994."},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In Proc. 7th FPCA, pages 170\u2013181. ACM Press, 1995.","DOI":"10.1145\/224164.224199"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form, invited paper. In P. Wolper, editor, Proc. 7th Int. Conf. CAV '95. LNCS 939, pages 293\u2013308. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60045-0_58"},{"key":"1_CR24","unstructured":"P. Cousot, R. Cousot, and A. Mycroft. Report on a Dagsthul seminar on abstract interpretation, 1995."},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"P. Cousot: Abstract Interpretation. Computing Surveys 28 2, pages 324\u2013328, ACM Press, 1996.","DOI":"10.1145\/234528.234740"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"P. Cousot. Types as abstract interpretation. In 24th POPL. ACM Press, 1997.","DOI":"10.1145\/263699.263744"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"R. Cridlig. Semantic analysis of shared-memory concurrent languages using abstract model-checking. In Proc. PEPM '95. ACM Press, 1995.","DOI":"10.1145\/215465.215593"},{"key":"1_CR28","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1007\/3-540-60218-6_2","volume":"962","author":"M. Dam","year":"1995","unstructured":"M. Dam. Compositional proof systems for model checking infinite state processes. In Proc. CONCUR'95, Lecture Notes in Computer Science, 962:12\u201326, 1995.","journal-title":"Lecture Notes in Computer Science"},{"key":"1_CR29","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1006\/inco.1996.0072","volume":"129","author":"M. Dam","year":"1996","unstructured":"M. Dam. Model checking mobile processes. Information and Computation, 129:35\u201351, 1996.","journal-title":"Information and Computation"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"M. Dam: Modalities in Analysis and Verification. ACM Computing Surveys 28 2, pages 346\u2013348, ACM Press, 1996.","DOI":"10.1145\/234528.234746"},{"key":"1_CR31","unstructured":"M. Dam. Compositional verification of mobile process networks. In preparation, 1997."},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"P. Degano, R. De Nicola, and U. Montanari. Partial ordering derivations for CCS. In Proceedings of FCT, LNCS 199, pages 520\u2013533. Springer-Verlag, 1985.","DOI":"10.1007\/BFb0028836"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"P. Degano and C. Priami. Proved trees. In Proceedings of ICALP'92, LNCS 623, pages 629\u2013640. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55719-9_110"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"P. Degano and C. Priami. Causality for mobile processes. In Proceedings of ICALP'95, LNCS 944, pages 660\u2013671. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60084-1_113"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"P. Degano and C. Priami: Enhanced Operational Semantics. Computing Surveys 28 2, pages 352\u2013354, ACM Press, 1996.","DOI":"10.1145\/234528.234748"},{"key":"1_CR36","unstructured":"P. Degano and C. Priami: A Compact Representation of Finite State Processes. Report available via http:\/\/www.daimi.aau.dk\/\u223cbra8130\/LOMAPS-papers.html by selection of LOMAPS-DIPISA-2."},{"key":"1_CR37","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E. A. Emerson","year":"1996","unstructured":"E. A. Emerson and A.P. Sistla. Symmetry and model checking. Formal Methods in System Design, 9:105\u2013131, 1996.","journal-title":"Formal Methods in System Design"},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"J. Esparza. Decidability of model checking for infinite-state concurrent systems. Acta Informatica, 1996. (to appear).","DOI":"10.1007\/s002360050074"},{"key":"1_CR39","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF01491213","volume":"18","author":"A. Giacalone","year":"1989","unstructured":"A. Giacalone, P. Mishra, and S. Prasad. Facile: A symmetric integration of concurrent and functional programming. International Journal of Parallel Programming, 18:121\u2013160, 1989.","journal-title":"International Journal of Parallel Programming"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"E. Goubault. Durations for truly-concurrent actions. In Proceedings of ESOP'96, LNCS, 1058, pages 173\u2013187. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61055-3_36"},{"key":"1_CR41","volume-title":"The Java language environment. White paper","author":"J. Gosling","year":"1995","unstructured":"J. Gosling and H. McGilton. The Java language environment. White paper, May 1995. Sun Microsystems, 2550 Garcia Avenue, Mountain View, CA 94043, USA."},{"key":"1_CR42","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1145\/215465.215577","volume-title":"Proc. PEPM '95","author":"E. Goubault","year":"1995","unstructured":"E. Goubault. Schedulers as abstract interpretations of higher-dimensional automata. In Proc. PEPM '95, La Jolla, Calif., 21\u201323 jun 1995, pages 134\u2013145. ACM Press, jun 1995."},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"G. J. Holzmann. An analysis of bitstate hashing. In Proc. PSTV'95, Chapman and Hall, pages 301\u2013314, 1995.","DOI":"10.1007\/978-0-387-34892-6_19"},{"issue":"6","key":"1_CR44","doi-asserted-by":"crossref","first-page":"676","DOI":"10.1007\/BF03259392","volume":"6","author":"P. Inverardi","year":"1994","unstructured":"P. Inverardi, C. Priami, and D. Yankelevich. Automatizing parametric reasoning on distributed concurrent systems. Formal Aspects of Computing, 6(6):676\u2013695, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"1_CR45","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/3-540-55253-7_17","volume":"582","author":"M. P. Jones","year":"1992","unstructured":"M. P. Jones. A theory of qualified types. In Proc. ESOP '92, pages 287\u2013306, Springer Lecture Notes in Computer Science 582, 1992.","journal-title":"Springer Lecture Notes in Computer Science"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"N. D. Jones and F. Nielson. Abstract Interpretation: a Semantics-Based Tool for Program Analysis. In Handbook of Logic in Computer Science volume 4. Oxford University Press, 1995.","DOI":"10.1093\/oso\/9780198537809.003.0005"},{"key":"1_CR47","unstructured":"F. Levi. Verification of Temporal and Real-Time Properties of Statecharts. PhD Thesis in Computer Science, University of Pisa, to be discussed in January 1997."},{"key":"1_CR48","unstructured":"P. Lucas. Formal definition of programming languages and systems. In Springer Verlag, editor, Proceedings of IFIP'71, 1971."},{"key":"1_CR49","doi-asserted-by":"crossref","unstructured":"A. Maggiolo-Schettini and A. Peron Retiming Techniques for Statecharts In Proc. FTRTFT '96, LNCS 1135, pages 55\u201371. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61648-9_34"},{"key":"1_CR50","doi-asserted-by":"crossref","unstructured":"A. Maggiolo-Schettini, A. Peron and S. Tini Equivalences of Statecharts In Proc. CONCUR '96, LNCS 1119, pages 687\u2013702. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61604-7_84"},{"key":"1_CR51","doi-asserted-by":"crossref","unstructured":"L. Mauborgne. Abstract interpretation using TDGs. In B. Le Charlier, editor, Proc. SAS '94, Namur, 20\u201322 sep 1994, LNCS 864, pages 363\u2013379. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58485-4_52"},{"key":"1_CR52","unstructured":"J. McCarthy. Towards a mathematical science of computation. In C.M. Popplewell, editor, Information Processing 1962, pages 21\u201328, 1963."},{"key":"1_CR53","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"issue":"1","key":"1_CR54","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes (I and II). Information and Computation, 100(1):1\u201377, 1992.","journal-title":"Information and Computation"},{"key":"1_CR55","doi-asserted-by":"crossref","unstructured":"B. Monsuez. Polymorphic types and widening operators. In P. Cousot, M. Falaschi, G. Fil\u00e9, and A. Rauzy, editors, Proc. 3rd Int. Work. WSA '93 on Static Analysis. LNCS 724, pages 267\u2013281. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57264-3_47"},{"key":"1_CR56","doi-asserted-by":"crossref","unstructured":"B. Monsuez. Polymorphic typing for call-by-name semantics. In D. Bj\u00f8rner, M. Broy, and I.V. Pottosin, editors, Proc. FMPA. LNCS 735, pages 156\u2013169. Springer-Verlag, 1993.","DOI":"10.1007\/BFb0039706"},{"key":"1_CR57","doi-asserted-by":"crossref","unstructured":"B. Monsuez. System F and abstract interpretation. In A. Mycroft, editor, Proc. SAS '95. LNCS 983, pages 279\u2013295. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60360-3_45"},{"key":"1_CR58","doi-asserted-by":"crossref","unstructured":"B. Monsuez. Using abstract interpretation to define a strictness type inference system. In Proc. PEPM '95, pages 122\u2013133. ACM Press, 1995.","DOI":"10.1145\/215465.215574"},{"key":"1_CR59","doi-asserted-by":"crossref","unstructured":"A. Mycroft and F. Nielson. Strong Abstract Interpretation using Power Domains. In Proc. ICALP '83, volume 154, pages 536\u2013547. SLNCS, 1983.","DOI":"10.1007\/BFb0036935"},{"key":"1_CR60","doi-asserted-by":"crossref","unstructured":"A. Mycroft and K.L. Solberg. Uniform PERs and comportment analysis. PLILP'95, 1995.","DOI":"10.1007\/BFb0026820"},{"key":"1_CR61","doi-asserted-by":"crossref","unstructured":"A. Mycroft: On Integration of Programming Paradigms. ACM Computing Surveys 28 2, pages 309\u2013311, ACM Press, 1996.","DOI":"10.1145\/234528.234735"},{"key":"1_CR62","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/0304-3975(89)90091-1","volume":"69","author":"F. Nielson","year":"1989","unstructured":"F. Nielson. Two-Level Semantics and Abstract Interpretation. Theoretical Computer Science \u2014 Fundamental Studies, 69:117\u2013242, 1989.","journal-title":"Theoretical Computer Science \u2014 Fundamental Studies"},{"key":"1_CR63","unstructured":"F. Nielson and H.R. Nielson. Semantics with applications: a formal introduction. Wiley, 1992."},{"key":"1_CR64","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/3-540-56596-5_43","volume":"666","author":"F Nielson","year":"1993","unstructured":"F Nielson and H.R. Nielson. Layered Predicates. In Proc. REX'92 workshop on \u201cSemantics\u2014foundations and applications\u201d, pages 425\u2013456, Springer Lecture Notes in Computer Science 666, 1993.","journal-title":"Springer Lecture Notes in Computer Science"},{"key":"1_CR65","doi-asserted-by":"crossref","unstructured":"H. R. Nielson and F. Nielson. Higher-Order Concurrent Programs with Finite Communication Topology. In Proc. POPL '94, pages 84\u201397, ACM Press, 1994.","DOI":"10.1145\/174675.174538"},{"key":"1_CR66","doi-asserted-by":"crossref","unstructured":"F. Nielson: Annotated Type and Effect Systems. ACM Computing Surveys 28 2, pages 344\u2013345, ACM Press, 1996.","DOI":"10.1145\/234528.234745"},{"key":"1_CR67","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-61739-6_30","volume":"1145","author":"F Nielson","year":"1996","unstructured":"F Nielson. Semantics-Directed Program Analysis: A Tool-Maker's Perspective. In Proc. SAS'96, pages 2\u201321, Springer Lecture Notes in Computer Science 1145, 1996.","journal-title":"Springer Lecture Notes in Computer Science"},{"key":"1_CR68","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume":"1102","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. K. Srivas. PVS: Combining specification, proof checking, and model checking. In Proc. CAV'96, Lecture Notes in Computer Science, 1102:411\u2013414, 1996.","journal-title":"Lecture Notes in Computer Science"},{"key":"1_CR69","unstructured":"B. Pierce and D. Turner. PICT Language Definition. University of Indiana, December 1995."},{"key":"1_CR70","doi-asserted-by":"crossref","unstructured":"B. C. Pierce and D. N. Turner. Concurrent objects in a process calculus. In Theory and Practice of Parallel Programming, volume 907 of Lecture Notes in Computer Science. Springer-Verlag, April 1995.","DOI":"10.1007\/BFb0026570"},{"key":"1_CR71","volume-title":"Technical Report DAIMI FN-19","author":"G. Plotkin","year":"1981","unstructured":"G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, Denmark, 1981."},{"issue":"6","key":"1_CR72","doi-asserted-by":"crossref","first-page":"578","DOI":"10.1093\/comjnl\/38.7.578","volume":"38","author":"C. Priami","year":"1995","unstructured":"C. Priami. Stochastic \u03c0-calculus. The Computer Journal, 38(6): 578\u2013589, 1995.","journal-title":"The Computer Journal"},{"key":"1_CR73","unstructured":"C. Priami. Enhanced Operational Semantics for Concurrency. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, March 1996. Available as Tech. Rep. TD-08\/96."},{"key":"1_CR74","first-page":"508","volume-title":"Integrating behavioural and performance analysis with topology information","author":"C. Priami","year":"1996","unstructured":"C. Priami. Integrating behavioural and performance analysis with topology information. In Proceedings of 29 th Hawaian International Conference on System Sciences, volume 1, pages 508\u2013516, Maui, Hawaii, 1996. IEEE."},{"key":"1_CR75","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/3-540-61474-5_70","volume":"1102","author":"H. B. Sipma","year":"1996","unstructured":"H. B. Sipma, T. E. Uribe, and Z. Manna. Deductive model checking. In Proc. CAV'96, Lecture Notes in Computer Science, 1102:208\u2013219, 1996.","journal-title":"Lecture Notes in Computer Science"},{"key":"1_CR76","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/0167-6423(94)00020-4","volume":"23","author":"G. S. Smith","year":"1994","unstructured":"G. S. Smith. Principal Type Schemes for Functional Programs with Overloading and Subtyping. Science of Computer Programming 23, pages 197\u2013226, 1994.","journal-title":"Science of Computer Programming"},{"key":"1_CR77","doi-asserted-by":"crossref","unstructured":"G. Smolka. The definition of kernal Oz, in Constraints: Basic and Trends, Lecture Notes in Computer Science 910. Springer Verlag, 1995.","DOI":"10.1007\/3-540-59155-9_14"},{"key":"1_CR78","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/0304-3975(87)90012-0","volume":"49","author":"C. Stirling","year":"1987","unstructured":"C. Stirling. Modal logics for communicating systems. Theoretical Computer Science, 49:311\u2013347, 1987.","journal-title":"Theoretical Computer Science"},{"key":"1_CR79","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1006\/inco.1994.1046","volume":"111","author":"J.-P. Talpin","year":"1994","unstructured":"J.-P. Talpin and P. Jouvelot. The type and effect discipline. Information and Computation 111, pages 245\u2013296, 1994.","journal-title":"Information and Computation"},{"key":"1_CR80","doi-asserted-by":"crossref","unstructured":"B. Thomsen, L. Leth, and T.-M. Kuo. A Facile tutorial. In Proceedings of CON-CUR'96 \u2014 Seventh Intl. Conf. on Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 278\u2013298. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61604-7_61"},{"key":"1_CR81","unstructured":"B. Thomsen, F. Knabe, L. Leth and P.-Y. Chevalier. Mobile Agents Set to Work, In Communications International, July, 1995."},{"key":"1_CR82","doi-asserted-by":"crossref","unstructured":"M. Tofte and J.-P. Talpin: Implementation of the Typed Call-by-Value \u03bb-Calculus using a Stack of Regions. In Proc. POPL '94, pages 188\u2013210, ACM Press, 1994.","DOI":"10.1145\/174675.177855"},{"key":"1_CR83","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A. Valmari","year":"1992","unstructured":"A. Valmari. A stubborn attack on state explosion. Formal Methods in System Design, 1:297\u2013322, 1992.","journal-title":"Formal Methods in System Design"},{"key":"1_CR84","doi-asserted-by":"crossref","unstructured":"F. V\u00e9drine. Binding-time analysis and strictness analysis by abstract interpretation. In A. Mycroft, editor, Proc. SAS '95. LNCS 983, pages 400\u2013417. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60360-3_52"},{"key":"1_CR85","doi-asserted-by":"crossref","unstructured":"A. Venet. Abstract cofibred domains: Application to the alias analysis of untyped programs. In R. Cousot and D.A. Schmidt, editors, Proc. SAS'96. LNCS 1145, pages 368\u2013382. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61739-6_53"},{"key":"1_CR86","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-61474-5_58","volume":"1102","author":"I. Walukiewicz","year":"1996","unstructured":"I. Walukiewicz. Pushdown processes: Games and model checking. In Proc. CAV'96, Lecture Notes in Computer Science, 1102:62\u201374, 1996.","journal-title":"Lecture Notes in Computer Science"},{"key":"1_CR87","unstructured":"J. E. White. \u201dTelescript technology: The foundation for the electronic market place\u201d. General Magic white paper, 2465 Latham Street, Mountain View, CA 94040, 1994."},{"key":"1_CR88","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/3-540-57208-2_17","volume":"715","author":"P. Wolper","year":"1993","unstructured":"P. Wolper and P. Godefroid. Partial-order methods for temporal verification. In Proc. CONCUR'93, Lecture Notes in Computer Science, 715:233\u2013246, 1993.","journal-title":"Lecture Notes in Computer Science"}],"container-title":["Lecture Notes in Computer Science","Analysis and Verification of Multiple-Agent Languages"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62503-8_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:53:55Z","timestamp":1713635635000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62503-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540625032","9783540680529"],"references-count":88,"URL":"https:\/\/doi.org\/10.1007\/3-540-62503-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}